toComplex_inv

formal source

 105    toComplex (z * w) = toComplex z * toComplex w := by
 106  simp [HMul.hMul, Mul.mul]
 107
 108@[simp] theorem toComplex_inv (z : LogicComplex) :
 109    toComplex z⁻¹ = (toComplex z)⁻¹ := by
 110  simp [Inv.inv]
 111
 112@[simp] theorem toComplex_div (z w : LogicComplex) :
 113    toComplex (z / w) = toComplex z / toComplex w := by
 114  simp [HDiv.hDiv, Div.div]
 115
 116/-- Embed recovered reals into recovered complex numbers. -/
 117def ofLogicReal (x : LogicReal) : LogicComplex where
 118  re := x
 119  im := 0
 120
 121@[simp] theorem toComplex_ofLogicReal (x : LogicReal) :
 122    toComplex (ofLogicReal x) = (toReal x : ℂ) := by
 123  apply Complex.ext <;> simp [ofLogicReal, toComplex]
 124
 125/-- Embed recovered rationals into recovered complex numbers through recovered
 126reals. -/
 127def ofLogicRat (q : RationalsFromLogic.LogicRat) : LogicComplex :=
 128  ofLogicReal (RealsFromLogic.LogicReal.ofLogicRat q)
 129
 130@[simp] theorem toComplex_ofLogicRat (q : RationalsFromLogic.LogicRat) :
 131    toComplex (ofLogicRat q) = ((RationalsFromLogic.LogicRat.toRat q : ℚ) : ℂ) := by
 132  rw [ofLogicRat, toComplex_ofLogicReal, toReal_ofLogicRat]
 133  norm_num
 134
 135/-- The recovered complex carrier is exactly Mathlib `ℂ`, by transport. -/
 136theorem logicComplex_recovered_from_mathlib :
 137    (∀ z : LogicComplex, fromComplex (toComplex z) = z) ∧
 138    (∀ z : ℂ, toComplex (fromComplex z) = z) :=