theorem
proved
toComplex_im
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 45.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
73 exact this
74
75/-! ## Algebra and coordinate transport -/