theorem
proved
toComplex_div
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 112.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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) :=
139 ⟨fromComplex_toComplex, toComplex_fromComplex⟩
140
141end LogicComplex
142