 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.