theorem
proved
toComplex_add
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ComplexFromLogic on GitHub at line 92.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
89@[simp] theorem toComplex_one : toComplex (1 : LogicComplex) = 1 := by
90 exact toComplex_fromComplex 1
91
92@[simp] theorem toComplex_add (z w : LogicComplex) :
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