theorem
proved
toComplex_ofLogicReal
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 121.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
143end
144
145end ComplexFromLogic
146end Foundation
147end IndisputableMonolith