theorem Mathlib.Meta.NormNumI.split_I : Complex.I = { re := 0, im := 1 }

theorem Mathlib.Meta.NormNumI.split_zero : 0 = { re := 0, im := 0 }

theorem Mathlib.Meta.NormNumI.split_one : 1 = { re := 1, im := 0 }

theorem Mathlib.Meta.NormNumI.split_add {z₁ z₂ : ℂ} {a₁ a₂ b₁ b₂ : ℝ} (h₁ : z₁ = { re := a₁, im := b₁ }) (h₂ : z₂ = { re := a₂, im := b₂ }) : z₁ + z₂ = { re := a₁ + a₂, im := b₁ + b₂ }

theorem Mathlib.Meta.NormNumI.split_mul {z₁ z₂ : ℂ} {a₁ a₂ b₁ b₂ : ℝ} (h₁ : z₁ = { re := a₁, im := b₁ }) (h₂ : z₂ = { re := a₂, im := b₂ }) : z₁ * z₂ = { re := a₁ * a₂ - b₁ * b₂, im := a₁ * b₂ + b₁ * a₂ }

theorem Mathlib.Meta.NormNumI.split_inv {z : ℂ} {x y : ℝ} (h : z = { re := x, im := y }) : z⁻¹ = { re := x / (x * x + y * y), im := -y / (x * x + y * y) }

theorem Mathlib.Meta.NormNumI.split_neg {z : ℂ} {a b : ℝ} (h : z = { re := a, im := b }) : -z = { re := -a, im := -b }

theorem Mathlib.Meta.NormNumI.split_conj {w : ℂ} {a b : ℝ} (hw : w = { re := a, im := b }) : (starRingEnd ℂ) w = { re := a, im := -b }

theorem Mathlib.Meta.NormNumI.split_num (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n = { re := OfNat.ofNat n, im := 0 }

theorem Mathlib.Meta.NormNumI.split_scientific (m exp : ℕ) (x : Bool) : OfScientific.ofScientific m x exp = { re := OfScientific.ofScientific m x exp, im := 0 }

theorem Mathlib.Meta.NormNumI.eq_eq {z : ℂ} {a b a' b' : ℝ} (pf : z = { re := a, im := b }) (pf_a : a = a') (pf_b : b = b') : z = { re := a', im := b' }

theorem Mathlib.Meta.NormNumI.eq_of_eq_of_eq_of_eq {z w : ℂ} {az bz aw bw : ℝ} (hz : z = { re := az, im := bz }) (hw : w = { re := aw, im := bw }) (ha : az = aw) (hb : bz = bw) : z = w

theorem Mathlib.Meta.NormNumI.ne_of_re_ne {z w : ℂ} {az bz aw bw : ℝ} (hz : z = { re := az, im := bz }) (hw : w = { re := aw, im := bw }) (ha : az ≠ aw) : z ≠ w

theorem Mathlib.Meta.NormNumI.ne_of_im_ne {z w : ℂ} {az bz aw bw : ℝ} (hz : z = { re := az, im := bz }) (hw : w = { re := aw, im := bw }) (hb : bz ≠ bw) : z ≠ w

theorem Mathlib.Meta.NormNumI.re_eq_of_eq {z : ℂ} {a b : ℝ} (hz : z = { re := a, im := b }) : z.re = a

theorem Mathlib.Meta.NormNumI.im_eq_of_eq {z : ℂ} {a b : ℝ} (hz : z = { re := a, im := b }) : z.im = b

partial def Mathlib.Meta.NormNumI.parse (z : Q(ℂ)) : Lean.MetaM ((a : Q(ℝ)) × (b : Q(ℝ)) × Q(«$z» = { re := «$a», im := «$b» }))

def Mathlib.Meta.NormNumI.normalize (z : Q(ℂ)) : Lean.MetaM ((a : Q(ℝ)) × (b : Q(ℝ)) × Q(«$z» = { re := «$a», im := «$b» }))

Equations

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

def Mathlib.Meta.NormNumI.convNorm_numI : Lean.ParserDescr

Equations

• Mathlib.Meta.NormNumI.convNorm_numI = Lean.ParserDescr.node `Mathlib.Meta.NormNumI.convNorm_numI 1024 (Lean.ParserDescr.nonReservedSymbol "norm_numI" false)

def Mathlib.Meta.NormNumI.convNorm_numI_parse : Lean.ParserDescr

Equations

• Mathlib.Meta.NormNumI.convNorm_numI_parse = Lean.ParserDescr.node `Mathlib.Meta.NormNumI.convNorm_numI_parse 1024 (Lean.ParserDescr.nonReservedSymbol "norm_numI_parse" false)

def Mathlib.Meta.NormNum.evalComplexEq : NormNumExt

The norm_num extension which identifies expressions of the form (z : ℂ) = (w : ℂ), such that norm_num successfully recognises both the real and imaginary parts of both z and w.

Equations

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

def Mathlib.Meta.NormNum.evalRe : NormNumExt

The norm_num extension which identifies expressions of the form Complex.re (z : ℂ), such that norm_num successfully recognises the real part of z.

Equations

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

def Mathlib.Meta.NormNum.evalIm : NormNumExt

The norm_num extension which identifies expressions of the form Complex.im (z : ℂ), such that norm_num successfully recognises the imaginary part of z.

Equations

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