theorem
proved
toComplex_neg
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 96.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
93 toComplex (z + w) = toComplex z + toComplex w := by
94 simp [HAdd.hAdd, Add.add]
95
96@[simp] theorem toComplex_neg (z : LogicComplex) :
97 toComplex (-z) = -toComplex z := by
98 simp [Neg.neg]
99
100@[simp] theorem toComplex_sub (z w : LogicComplex) :
101 toComplex (z - w) = toComplex z - toComplex w := by
102 simp [HSub.hSub, Sub.sub]
103
104@[simp] theorem toComplex_mul (z w : LogicComplex) :
105 toComplex (z * w) = toComplex z * toComplex w := by
106 simp [HMul.hMul, Mul.mul]
107
108@[simp] theorem toComplex_inv (z : LogicComplex) :
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. -/