# The complex numbers #

The complex numbers are modelled as ℝ^2 in the obvious way and it is shown that they form a field of characteristic zero. For the result that the complex numbers are algebraically closed, see `Complex.isAlgClosed` in `Mathlib.Analysis.Complex.Polynomial.Basic`.

### Definition and basic arithmetic #

source
structure Complex :
Type

Complex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.

- re : ℝ

  The real part of a complex number.

- im : ℝ

  The imaginary part of a complex number.

Instances For

source
def termℂ :
Lean.ParserDescr

Complex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`.

Equations

- termℂ = Lean.ParserDescr.node `termℂ 1024 (Lean.ParserDescr.symbol "ℂ")

Instances For

source
noncomputable instance Complex.instDecidableEq :
DecidableEq ℂ
Equations

- Complex.instDecidableEq = Classical.decEq ℂ

source
def Complex.equivRealProd :
ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and `ℝ × ℝ`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Complex.equivRealProd_apply (z : ℂ) :
equivRealProd z = (z.re, z.im)
source
@[simp]
theorem Complex.eta (z : ℂ) :
{ re := z.re, im := z.im } = z
source
theorem Complex.ext {z w : ℂ} :
z.re = w.re → z.im = w.im → z = w
source
theorem Complex.ext_iff {z w : ℂ} :
z = w ↔ z.re = w.re ∧ z.im = w.im
source
theorem Complex.forall {p : ℂ → Prop} :
(∀ (x : ℂ), p x) ↔ ∀ (a b : ℝ), p { re := a, im := b }
source
theorem Complex.exists {p : ℂ → Prop} :
(∃ (x : ℂ), p x) ↔ ∃ (a : ℝ) (b : ℝ), p { re := a, im := b }
source
theorem Complex.re_surjective :
Function.Surjective re
source
theorem Complex.im_surjective :
Function.Surjective im
source
@[simp]
theorem Complex.range_re :
Set.range re = Set.univ
source
@[simp]
theorem Complex.range_im :
Set.range im = Set.univ
source
def Complex.ofReal (r : ℝ) :
ℂ

The natural inclusion of the real numbers into the complex numbers.

Equations

- ↑r = { re := r, im := 0 }

Instances For

source
instance Complex.instCoeReal :
Coe ℝ ℂ
Equations

- Complex.instCoeReal = { coe := Complex.ofReal }

source
@[simp]
theorem Complex.ofReal_re (r : ℝ) :
(↑r).re = r
source
@[simp]
theorem Complex.ofReal_im (r : ℝ) :
(↑r).im = 0
source
theorem Complex.ofReal_def (r : ℝ) :
↑r = { re := r, im := 0 }
source
@[simp]
theorem Complex.ofReal_inj {z w : ℝ} :
↑z = ↑w ↔ z = w
source
theorem Complex.ofReal_injective :
Function.Injective ofReal
source
instance Complex.canLift :
CanLift ℂ ℝ ofReal fun (z : ℂ) => z.im = 0
source
def Complex.reProdIm (s t : Set ℝ) :
Set ℂ

The product of a set on the real axis and a set on the imaginary axis of the complex plane, denoted by `s ×ℂ t`.

Equations

- s ×ℂ t = Complex.re ⁻¹' s ∩ Complex.im ⁻¹' t

Instances For

source
def Complex.«term_×ℂ_» :
Lean.TrailingParserDescr

The product of a set on the real axis and a set on the imaginary axis of the complex plane, denoted by `s ×ℂ t`.

Equations

- Complex.«term_×ℂ_» = Lean.ParserDescr.trailingNode `Complex.«term_×ℂ_» 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ℂ ") (Lean.ParserDescr.cat `term 73))

Instances For

source
theorem Complex.mem_reProdIm {z : ℂ} {s t : Set ℝ} :
z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t
source
instance Complex.instZero :
Zero ℂ
Equations

- Complex.instZero = { zero := ↑0 }

source
instance Complex.instInhabited :
Inhabited ℂ
Equations

- Complex.instInhabited = { default := 0 }

source
@[simp]
theorem Complex.zero_re :
re 0 = 0
source
@[simp]
theorem Complex.zero_im :
im 0 = 0
source
@[simp]
theorem Complex.ofReal_zero :
↑0 = 0
source
@[simp]
theorem Complex.ofReal_eq_zero {z : ℝ} :
↑z = 0 ↔ z = 0
source
theorem Complex.ofReal_ne_zero {z : ℝ} :
↑z ≠ 0 ↔ z ≠ 0
source
instance Complex.instOne :
One ℂ
Equations

- Complex.instOne = { one := ↑1 }

source
@[simp]
theorem Complex.one_re :
re 1 = 1
source
@[simp]
theorem Complex.one_im :
im 1 = 0
source
@[simp]
theorem Complex.ofReal_one :
↑1 = 1
source
@[simp]
theorem Complex.ofReal_eq_one {z : ℝ} :
↑z = 1 ↔ z = 1
source
theorem Complex.ofReal_ne_one {z : ℝ} :
↑z ≠ 1 ↔ z ≠ 1
source
instance Complex.instAdd :
Add ℂ
Equations

- Complex.instAdd = { add := fun (z w : ℂ) => { re := z.re + w.re, im := z.im + w.im } }

source
@[simp]
theorem Complex.add_re (z w : ℂ) :
(z + w).re = z.re + w.re
source
@[simp]
theorem Complex.add_im (z w : ℂ) :
(z + w).im = z.im + w.im
source
@[simp]
theorem Complex.ofReal_add (r s : ℝ) :
↑(r + s) = ↑r + ↑s
source
instance Complex.instNeg :
Neg ℂ
Equations

- Complex.instNeg = { neg := fun (z : ℂ) => { re := -z.re, im := -z.im } }

source
@[simp]
theorem Complex.neg_re (z : ℂ) :
(-z).re = -z.re
source
@[simp]
theorem Complex.neg_im (z : ℂ) :
(-z).im = -z.im
source
@[simp]
theorem Complex.ofReal_neg (r : ℝ) :
↑(-r) = -↑r
source
instance Complex.instSub :
Sub ℂ
Equations

- Complex.instSub = { sub := fun (z w : ℂ) => { re := z.re - w.re, im := z.im - w.im } }

source
instance Complex.instMul :
Mul ℂ
Equations

- Complex.instMul = { mul := fun (z w : ℂ) => { re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re } }

source
@[simp]
theorem Complex.mul_re (z w : ℂ) :
(z * w).re = z.re * w.re - z.im * w.im
source
@[simp]
theorem Complex.mul_im (z w : ℂ) :
(z * w).im = z.re * w.im + z.im * w.re
source
@[simp]
theorem Complex.ofReal_mul (r s : ℝ) :
↑(r * s) = ↑r * ↑s
source
theorem Complex.re_ofReal_mul (r : ℝ) (z : ℂ) :
(↑r * z).re = r * z.re
source
theorem Complex.im_ofReal_mul (r : ℝ) (z : ℂ) :
(↑r * z).im = r * z.im
source
theorem Complex.re_mul_ofReal (z : ℂ) (r : ℝ) :
(z * ↑r).re = z.re * r
source
theorem Complex.im_mul_ofReal (z : ℂ) (r : ℝ) :
(z * ↑r).im = z.im * r
source
theorem Complex.ofReal_mul' (r : ℝ) (z : ℂ) :
↑r * z = { re := r * z.re, im := r * z.im }

### The imaginary unit, `I` #

source
def Complex.I :
ℂ

The imaginary unit.

Equations

- Complex.I = { re := 0, im := 1 }

Instances For

source
@[simp]
theorem Complex.I_re :
I.re = 0
source
@[simp]
theorem Complex.I_im :
I.im = 1
source
@[simp]
theorem Complex.I_mul_I :
I * I = -1
source
theorem Complex.I_mul (z : ℂ) :
I * z = { re := -z.im, im := z.re }
source
@[simp]
theorem Complex.I_ne_zero :
I ≠ 0
source
theorem Complex.mk_eq_add_mul_I (a b : ℝ) :
{ re := a, im := b } = ↑a + ↑b * I
source
@[simp]
theorem Complex.re_add_im (z : ℂ) :
↑z.re + ↑z.im * I = z
source
theorem Complex.mul_I_re (z : ℂ) :
(z * I).re = -z.im
source
theorem Complex.mul_I_im (z : ℂ) :
(z * I).im = z.re
source
theorem Complex.I_mul_re (z : ℂ) :
(I * z).re = -z.im
source
theorem Complex.I_mul_im (z : ℂ) :
(I * z).im = z.re
source
@[simp]
theorem Complex.equivRealProd_symm_apply (p : ℝ × ℝ) :
equivRealProd.symm p = ↑p.1 + ↑p.2 * I
source
def Complex.equivRealProdAddHom :
ℂ ≃+ ℝ × ℝ

The natural `AddEquiv` from `ℂ` to `ℝ × ℝ`.

Equations

- Complex.equivRealProdAddHom = { toEquiv := Complex.equivRealProd, map_add' := Complex.equivRealProdAddHom._proof_1 }

Instances For

source
@[simp]
theorem Complex.equivRealProdAddHom_symm_apply_re (p : ℝ × ℝ) :
(equivRealProdAddHom.symm p).re = p.1
source
@[simp]
theorem Complex.equivRealProdAddHom_symm_apply_im (p : ℝ × ℝ) :
(equivRealProdAddHom.symm p).im = p.2
source
@[simp]
theorem Complex.equivRealProdAddHom_apply (z : ℂ) :
equivRealProdAddHom z = (z.re, z.im)
source
theorem Complex.equivRealProdAddHom_symm_apply (p : ℝ × ℝ) :
equivRealProdAddHom.symm p = ↑p.1 + ↑p.2 * I

### Commutative ring instance and lemmas #

source
instance Complex.instNontrivial :
Nontrivial ℂ
source
def Complex.SMul.instSMulRealComplex {R : Type u_1} [SMul R ℝ] :
SMul R ℂ

Scalar multiplication by `R` on `ℝ` extends to `ℂ`. This is used here and in `Mathlib/Data/Complex/Module.lean` to transfer instances from `ℝ` to `ℂ`, but is not needed outside, so we make it scoped.

Equations

- Complex.SMul.instSMulRealComplex = { smul := fun (r : R) (x : ℂ) => { re := r • x.re - 0 * x.im, im := r • x.im + 0 * x.re } }

Instances For

source
theorem Complex.smul_re {R : Type u_1} [SMul R ℝ] (r : R) (z : ℂ) :
(r • z).re = r • z.re
source
theorem Complex.smul_im {R : Type u_1} [SMul R ℝ] (r : R) (z : ℂ) :
(r • z).im = r • z.im
source
@[simp]
theorem Complex.real_smul {x : ℝ} {z : ℂ} :
x • z = ↑x * z
source
instance Complex.addCommGroup :
AddCommGroup ℂ
Equations

- One or more equations did not get rendered due to their size.

### Casts #

source
instance Complex.instNatCast :
NatCast ℂ
Equations

- Complex.instNatCast = { natCast := fun (n : ℕ) => ↑↑n }

source
instance Complex.instIntCast :
IntCast ℂ
Equations

- Complex.instIntCast = { intCast := fun (n : ℤ) => ↑↑n }

source
instance Complex.instNNRatCast :
NNRatCast ℂ
Equations

- Complex.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => ↑↑q }

source
instance Complex.instRatCast :
RatCast ℂ
Equations

- Complex.instRatCast = { ratCast := fun (q : ℚ) => ↑↑q }

source
@[simp]
theorem Complex.ofReal_ofNat (n : ℕ) [n.AtLeastTwo] :
↑(OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem Complex.ofReal_natCast (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem Complex.ofReal_intCast (n : ℤ) :
↑↑n = ↑n
source
@[simp]
theorem Complex.ofReal_nnratCast (q : ℚ≥0) :
↑↑q = ↑q
source
@[simp]
theorem Complex.ofReal_ratCast (q : ℚ) :
↑↑q = ↑q
source
@[simp]
theorem Complex.re_ofNat (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n).re = OfNat.ofNat n
source
@[simp]
theorem Complex.im_ofNat (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n).im = 0
source
@[simp]
theorem Complex.natCast_re (n : ℕ) :
(↑n).re = ↑n
source
@[simp]
theorem Complex.natCast_im (n : ℕ) :
(↑n).im = 0
source
@[simp]
theorem Complex.intCast_re (n : ℤ) :
(↑n).re = ↑n
source
@[simp]
theorem Complex.intCast_im (n : ℤ) :
(↑n).im = 0
source
@[simp]
theorem Complex.re_nnratCast (q : ℚ≥0) :
(↑q).re = ↑q
source
@[simp]
theorem Complex.im_nnratCast (q : ℚ≥0) :
(↑q).im = 0
source
@[simp]
theorem Complex.ratCast_re (q : ℚ) :
(↑q).re = ↑q
source
@[simp]
theorem Complex.ratCast_im (q : ℚ) :
(↑q).im = 0

### Ring structure #

source
instance Complex.addGroupWithOne :
AddGroupWithOne ℂ
Equations

- One or more equations did not get rendered due to their size.

source
instance Complex.commRing :
CommRing ℂ
Equations

- One or more equations did not get rendered due to their size.

source
instance Complex.instRing :
Ring ℂ

This shortcut instance ensures we do not find `Ring` via the noncomputable `Complex.field` instance.

Equations

- Complex.instRing = inferInstance

source
instance Complex.instCommSemiring :
CommSemiring ℂ

This shortcut instance ensures we do not find `CommSemiring` via the noncomputable `Complex.field` instance.

Equations

- Complex.instCommSemiring = inferInstance

source
instance Complex.instSemiring :
Semiring ℂ

This shortcut instance ensures we do not find `Semiring` via the noncomputable `Complex.field` instance.

Equations

- Complex.instSemiring = inferInstance

source
def Complex.reAddGroupHom :
ℂ →+ ℝ

The "real part" map, considered as an additive group homomorphism.

Equations

- Complex.reAddGroupHom = { toFun := Complex.re, map_zero' := Complex.zero_re, map_add' := Complex.add_re }

Instances For

source
@[simp]
theorem Complex.coe_reAddGroupHom :
⇑reAddGroupHom = re
source
def Complex.imAddGroupHom :
ℂ →+ ℝ

The "imaginary part" map, considered as an additive group homomorphism.

Equations

- Complex.imAddGroupHom = { toFun := Complex.im, map_zero' := Complex.zero_im, map_add' := Complex.add_im }

Instances For

source
@[simp]
theorem Complex.coe_imAddGroupHom :
⇑imAddGroupHom = im
source
theorem Complex.re_nsmul (n : ℕ) (z : ℂ) :
(n • z).re = n • z.re
source
theorem Complex.im_nsmul (n : ℕ) (z : ℂ) :
(n • z).im = n • z.im
source
theorem Complex.re_zsmul (n : ℤ) (z : ℂ) :
(n • z).re = n • z.re
source
theorem Complex.im_zsmul (n : ℤ) (z : ℂ) :
(n • z).im = n • z.im
source
@[simp]
theorem Complex.re_nnqsmul (q : ℚ≥0) (z : ℂ) :
(q • z).re = q • z.re
source
@[simp]
theorem Complex.im_nnqsmul (q : ℚ≥0) (z : ℂ) :
(q • z).im = q • z.im
source
@[simp]
theorem Complex.re_qsmul (q : ℚ) (z : ℂ) :
(q • z).re = q • z.re
source
@[simp]
theorem Complex.im_qsmul (q : ℚ) (z : ℂ) :
(q • z).im = q • z.im
source
theorem Complex.ofReal_nsmul (n : ℕ) (r : ℝ) :
↑(n • r) = n • ↑r
source
theorem Complex.ofReal_zsmul (n : ℤ) (r : ℝ) :
↑(n • r) = n • ↑r

### Complex conjugation #

source
instance Complex.instStarRing :
StarRing ℂ

This defines the complex conjugate as the `star` operation of the `StarRing ℂ`. It is recommended to use the ring endomorphism version `starRingEnd`, available under the notation `conj` in the scope `ComplexConjugate`.

Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Complex.conj_re (z : ℂ) :
((starRingEnd ℂ) z).re = z.re
source
@[simp]
theorem Complex.conj_im (z : ℂ) :
((starRingEnd ℂ) z).im = -z.im
source
@[simp]
theorem Complex.conj_ofReal (r : ℝ) :
(starRingEnd ℂ) ↑r = ↑r
source
@[simp]
theorem Complex.conj_I :
(starRingEnd ℂ) I = -I
source
theorem Complex.conj_natCast (n : ℕ) :
(starRingEnd ℂ) ↑n = ↑n
source
theorem Complex.conj_ofNat (n : ℕ) [n.AtLeastTwo] :
(starRingEnd ℂ) (OfNat.ofNat n) = OfNat.ofNat n
source
theorem Complex.conj_neg_I :
(starRingEnd ℂ) (-I) = I
source
theorem Complex.conj_eq_iff_real {z : ℂ} :
(starRingEnd ℂ) z = z ↔ ∃ (r : ℝ), z = ↑r
source
theorem Complex.conj_eq_iff_re {z : ℂ} :
(starRingEnd ℂ) z = z ↔ ↑z.re = z
source
theorem Complex.conj_eq_iff_im {z : ℂ} :
(starRingEnd ℂ) z = z ↔ z.im = 0
source
@[simp]
theorem Complex.star_def :
star = ⇑(starRingEnd ℂ)

### Norm squared #

source
def Complex.normSq :
ℂ →*₀ ℝ

The norm squared function.

Equations

- Complex.normSq = { toFun := fun (z : ℂ) => z.re * z.re + z.im * z.im, map_zero' := Complex.normSq._proof_1, map_one' := Complex.normSq._proof_2, map_mul' := Complex.normSq._proof_3 }

Instances For

source
theorem Complex.normSq_apply (z : ℂ) :
normSq z = z.re * z.re + z.im * z.im
source
@[simp]
theorem Complex.normSq_ofReal (r : ℝ) :
normSq ↑r = r * r
source
@[simp]
theorem Complex.normSq_natCast (n : ℕ) :
normSq ↑n = ↑n * ↑n
source
@[simp]
theorem Complex.normSq_intCast (z : ℤ) :
normSq ↑z = ↑z * ↑z
source
@[simp]
theorem Complex.normSq_ratCast (q : ℚ) :
normSq ↑q = ↑q * ↑q
source
@[simp]
theorem Complex.normSq_ofNat (n : ℕ) [n.AtLeastTwo] :
normSq (OfNat.ofNat n) = OfNat.ofNat n * OfNat.ofNat n
source
@[simp]
theorem Complex.normSq_mk (x y : ℝ) :
normSq { re := x, im := y } = x * x + y * y
source
theorem Complex.normSq_add_mul_I (x y : ℝ) :
normSq (↑x + ↑y * I) = x ^ 2 + y ^ 2
source
theorem Complex.normSq_eq_conj_mul_self {z : ℂ} :
↑(normSq z) = (starRingEnd ℂ) z * z
source
theorem Complex.normSq_zero :
normSq 0 = 0
source
theorem Complex.normSq_one :
normSq 1 = 1
source
@[simp]
theorem Complex.normSq_I :
normSq I = 1
source
theorem Complex.normSq_nonneg (z : ℂ) :
0 ≤ normSq z
source
theorem Complex.normSq_eq_zero {z : ℂ} :
normSq z = 0 ↔ z = 0
source
@[simp]
theorem Complex.normSq_pos {z : ℂ} :
0 < normSq z ↔ z ≠ 0
source
@[simp]
theorem Complex.normSq_neg (z : ℂ) :
normSq (-z) = normSq z
source
@[simp]
theorem Complex.normSq_conj (z : ℂ) :
normSq ((starRingEnd ℂ) z) = normSq z
source
theorem Complex.normSq_mul (z w : ℂ) :
normSq (z * w) = normSq z * normSq w
source
theorem Complex.normSq_add (z w : ℂ) :
normSq (z + w) = normSq z + normSq w + 2 * (z * (starRingEnd ℂ) w).re
source
theorem Complex.re_sq_le_normSq (z : ℂ) :
z.re * z.re ≤ normSq z
source
theorem Complex.im_sq_le_normSq (z : ℂ) :
z.im * z.im ≤ normSq z
source
theorem Complex.mul_conj (z : ℂ) :
z * (starRingEnd ℂ) z = ↑(normSq z)
source
theorem Complex.add_conj (z : ℂ) :
z + (starRingEnd ℂ) z = ↑(2 * z.re)
source
def Complex.ofRealHom :
ℝ →+* ℂ

The coercion `ℝ → ℂ` as a `RingHom`.

Equations

- Complex.ofRealHom = { toFun := fun (x : ℝ) => ↑x, map_one' := Complex.ofReal_one, map_mul' := Complex.ofReal_mul, map_zero' := Complex.ofReal_zero, map_add' := Complex.ofReal_add }

Instances For

source
@[simp]
theorem Complex.ofRealHom_eq_coe (r : ℝ) :
ofRealHom r = ↑r
source
@[simp]
theorem Complex.ofReal_comp_add {α : Type u_1} (f g : α → ℝ) :
ofReal ∘ (f + g) = ofReal ∘ f + ofReal ∘ g
source
@[simp]
theorem Complex.ofReal_comp_sub {α : Type u_1} (f g : α → ℝ) :
ofReal ∘ (f - g) = ofReal ∘ f - ofReal ∘ g
source
@[simp]
theorem Complex.ofReal_comp_neg {α : Type u_1} (f : α → ℝ) :
ofReal ∘ (-f) = -ofReal ∘ f
source
theorem Complex.ofReal_comp_nsmul {α : Type u_1} (n : ℕ) (f : α → ℝ) :
ofReal ∘ (n • f) = n • ofReal ∘ f
source
theorem Complex.ofReal_comp_zsmul {α : Type u_1} (n : ℤ) (f : α → ℝ) :
ofReal ∘ (n • f) = n • ofReal ∘ f
source
@[simp]
theorem Complex.ofReal_comp_mul {α : Type u_1} (f g : α → ℝ) :
ofReal ∘ (f * g) = ofReal ∘ f * ofReal ∘ g
source
@[simp]
theorem Complex.ofReal_comp_pow {α : Type u_1} (f : α → ℝ) (n : ℕ) :
ofReal ∘ (f ^ n) = ofReal ∘ f ^ n
source
@[simp]
theorem Complex.I_sq :
I ^ 2 = -1
source
@[simp]
theorem Complex.I_pow_three :
I ^ 3 = -I
source
@[simp]
theorem Complex.I_pow_four :
I ^ 4 = 1
source
theorem Complex.I_pow_eq_pow_mod (n : ℕ) :
I ^ n = I ^ (n % 4)
source
@[simp]
theorem Complex.sub_re (z w : ℂ) :
(z - w).re = z.re - w.re
source
@[simp]
theorem Complex.sub_im (z w : ℂ) :
(z - w).im = z.im - w.im
source
@[simp]
theorem Complex.ofReal_sub (r s : ℝ) :
↑(r - s) = ↑r - ↑s
source
@[simp]
theorem Complex.ofReal_pow (r : ℝ) (n : ℕ) :
↑(r ^ n) = ↑r ^ n
source
theorem Complex.sub_conj (z : ℂ) :
z - (starRingEnd ℂ) z = ↑(2 * z.im) * I
source
theorem Complex.normSq_sub (z w : ℂ) :
normSq (z - w) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

### Inversion #

source
noncomputable instance Complex.instInv :
Inv ℂ
Equations

- Complex.instInv = { inv := fun (z : ℂ) => (starRingEnd ℂ) z * ↑(Complex.normSq z)⁻¹ }

source
theorem Complex.inv_def (z : ℂ) :
z⁻¹ = (starRingEnd ℂ) z * ↑(normSq z)⁻¹
source
@[simp]
theorem Complex.inv_re (z : ℂ) :
z⁻¹.re = z.re / normSq z
source
@[simp]
theorem Complex.inv_im (z : ℂ) :
z⁻¹.im = -z.im / normSq z
source
@[simp]
theorem Complex.ofReal_inv (r : ℝ) :
↑r⁻¹ = (↑r)⁻¹
source
theorem Complex.inv_zero :
0⁻¹ = 0
source
theorem Complex.mul_inv_cancel {z : ℂ} (h : z ≠ 0) :
z * z⁻¹ = 1
source
noncomputable instance Complex.instDivInvMonoid :
DivInvMonoid ℂ
Equations

- One or more equations did not get rendered due to their size.

source
theorem Complex.div_re (z w : ℂ) :
(z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w
source
theorem Complex.div_im (z w : ℂ) :
(z / w).im = z.im * w.re / normSq w - z.re * w.im / normSq w

### Field instance and lemmas #

source
noncomputable instance Complex.instField :
Field ℂ
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem Complex.ofReal_nnqsmul (q : ℚ≥0) (r : ℝ) :
↑(q • r) = q • ↑r
source
@[simp]
theorem Complex.ofReal_qsmul (q : ℚ) (r : ℝ) :
↑(q • r) = q • ↑r
source
theorem Complex.conj_inv (x : ℂ) :
(starRingEnd ℂ) x⁻¹ = ((starRingEnd ℂ) x)⁻¹
source
@[simp]
theorem Complex.ofReal_div (r s : ℝ) :
↑(r / s) = ↑r / ↑s
source
@[simp]
theorem Complex.ofReal_zpow (r : ℝ) (n : ℤ) :
↑(r ^ n) = ↑r ^ n
source
@[simp]
theorem Complex.div_I (z : ℂ) :
z / I = -(z * I)
source
@[simp]
theorem Complex.inv_I :
I⁻¹ = -I
source
theorem Complex.normSq_inv (z : ℂ) :
normSq z⁻¹ = (normSq z)⁻¹
source
theorem Complex.normSq_div (z w : ℂ) :
normSq (z / w) = normSq z / normSq w
source
theorem Complex.div_ofReal (z : ℂ) (x : ℝ) :
z / ↑x = { re := z.re / x, im := z.im / x }
source
theorem Complex.div_natCast (z : ℂ) (n : ℕ) :
z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }
source
theorem Complex.div_intCast (z : ℂ) (n : ℤ) :
z / ↑n = { re := z.re / ↑n, im := z.im / ↑n }
source
theorem Complex.div_ratCast (z : ℂ) (x : ℚ) :
z / ↑x = { re := z.re / ↑x, im := z.im / ↑x }
source
theorem Complex.div_ofNat (z : ℂ) (n : ℕ) [n.AtLeastTwo] :
z / OfNat.ofNat n = { re := z.re / OfNat.ofNat n, im := z.im / OfNat.ofNat n }
source
@[simp]
theorem Complex.div_ofReal_re (z : ℂ) (x : ℝ) :
(z / ↑x).re = z.re / x
source
@[simp]
theorem Complex.div_ofReal_im (z : ℂ) (x : ℝ) :
(z / ↑x).im = z.im / x
source
@[simp]
theorem Complex.div_natCast_re (z : ℂ) (n : ℕ) :
(z / ↑n).re = z.re / ↑n
source
@[simp]
theorem Complex.div_natCast_im (z : ℂ) (n : ℕ) :
(z / ↑n).im = z.im / ↑n
source
@[simp]
theorem Complex.div_intCast_re (z : ℂ) (n : ℤ) :
(z / ↑n).re = z.re / ↑n
source
@[simp]
theorem Complex.div_intCast_im (z : ℂ) (n : ℤ) :
(z / ↑n).im = z.im / ↑n
source
@[simp]
theorem Complex.div_ratCast_re (z : ℂ) (x : ℚ) :
(z / ↑x).re = z.re / ↑x
source
@[simp]
theorem Complex.div_ratCast_im (z : ℂ) (x : ℚ) :
(z / ↑x).im = z.im / ↑x
source
@[simp]
theorem Complex.div_ofNat_re (z : ℂ) (n : ℕ) [n.AtLeastTwo] :
(z / OfNat.ofNat n).re = z.re / OfNat.ofNat n
source
@[simp]
theorem Complex.div_ofNat_im (z : ℂ) (n : ℕ) [n.AtLeastTwo] :
(z / OfNat.ofNat n).im = z.im / OfNat.ofNat n

### Characteristic zero #

source
instance Complex.instCharZero :
CharZero ℂ
source
instance Complex.instIsAddTorsionFree :
IsAddTorsionFree ℂ
source
theorem Complex.re_eq_add_conj (z : ℂ) :
↑z.re = (z + (starRingEnd ℂ) z) / 2

A complex number `z` plus its conjugate `conj z` is `2` times its real part.

source
theorem Complex.im_eq_sub_conj (z : ℂ) :
↑z.im = (z - (starRingEnd ℂ) z) / (2 * I)

A complex number `z` minus its conjugate `conj z` is `2i` times its imaginary part.

source
unsafe instance Complex.instRepr :
Repr ℂ

Show the imaginary number ⟨x, y⟩ as an "x + y*I" string

Note that the Real numbers used for x and y will show as Cauchy sequences due to the way Real numbers are represented.

Equations

- One or more equations did not get rendered due to their size.

source
theorem Complex.preimage_equivRealProd_prod (s t : Set ℝ) :
⇑equivRealProd ⁻¹' s ×ˢ t = s ×ℂ t

The preimage under `equivRealProd` of `s ×ˢ t` is `s ×ℂ t`.

source
theorem Complex.reProdIm_subset_iff {s s₁ t t₁ : Set ℝ} :
s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁

The inequality `s × t ⊆ s₁ × t₁` holds in `ℂ` iff it holds in `ℝ × ℝ`.

source
theorem Complex.reProdIm_subset_iff' {s s₁ t t₁ : Set ℝ} :
s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅

If `s ⊆ s₁ ⊆ ℝ` and `t ⊆ t₁ ⊆ ℝ`, then `s × t ⊆ s₁ × t₁` in `ℂ`.

source
@[simp]
theorem Complex.reProdIm_nonempty {s t : Set ℝ} :
(s ×ℂ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
source
@[simp]
theorem Complex.reProdIm_eq_empty {s t : Set ℝ} :
s ×ℂ t = ∅ ↔ s = ∅ ∨ t = ∅
source
def Complex.Rectangle (z w : ℂ) :
Set ℂ

A `Rectangle` is an axis-parallel rectangle with corners `z` and `w`.

Equations

- z.Rectangle w = Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im

Instances For

source
theorem Complex.horizontalSegment_eq (a₁ a₂ b : ℝ) :
(fun (x : ℝ) => ↑x + ↑b * I) '' Set.uIcc a₁ a₂ = Set.uIcc a₁ a₂ ×ℂ {b}

A real segment `[a₁, a₂]` translated by `b * I` is the complex line segment.

source
theorem Complex.verticalSegment_eq (a b₁ b₂ : ℝ) :
(fun (y : ℝ) => ↑a + ↑y * I) '' Set.uIcc b₁ b₂ = {a} ×ℂ Set.uIcc b₁ b₂

A vertical segment `[b₁, b₂]` translated by `a` is the complex line segment.