theorem
proved
toComplex_re
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ComplexFromLogic on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
39 re := fromReal z.re
40 im := fromReal z.im
41
42@[simp] theorem toComplex_re (z : LogicComplex) :
43 (toComplex z).re = toReal z.re := rfl
44
45@[simp] theorem toComplex_im (z : LogicComplex) :
46 (toComplex z).im = toReal z.im := rfl
47
48@[simp] theorem toComplex_fromComplex (z : ℂ) :
49 toComplex (fromComplex z) = z := by
50 apply Complex.ext <;> simp [toComplex, fromComplex, toReal_fromReal]
51
52@[simp] theorem fromComplex_toComplex (z : LogicComplex) :
53 fromComplex (toComplex z) = z := by
54 cases z with
55 | mk re im =>
56 simp [toComplex, fromComplex, fromReal_toReal]
57
58/-- Carrier equivalence between recovered complex numbers and Mathlib `ℂ`. -/
59def equivComplex : LogicComplex ≃ ℂ where
60 toFun := toComplex
61 invFun := fromComplex
62 left_inv := fromComplex_toComplex
63 right_inv := toComplex_fromComplex
64
65/-- Equality transfer for recovered complex numbers. -/
66theorem eq_iff_toComplex_eq {z w : LogicComplex} :
67 z = w ↔ toComplex z = toComplex w := by
68 constructor
69 · exact congrArg toComplex
70 · intro h
71 have := congrArg fromComplex h
72 rw [fromComplex_toComplex, fromComplex_toComplex] at this