theorem
proved
toComplex_sub
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ComplexFromLogic on GitHub at line 100.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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. -/
127def ofLogicRat (q : RationalsFromLogic.LogicRat) : LogicComplex :=
128 ofLogicReal (RealsFromLogic.LogicReal.ofLogicRat q)
129
130@[simp] theorem toComplex_ofLogicRat (q : RationalsFromLogic.LogicRat) :