theorem
proved
toComplex_add
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 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