theorem
proved
toComplex_inv
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.ComplexFromLogic on GitHub at line 108.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
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) :=