toComplex_zero

formal source

  83instance : Inv LogicComplex := ⟨fun z => fromComplex (toComplex z)⁻¹⟩
  84instance : Div LogicComplex := ⟨fun z w => fromComplex (toComplex z / toComplex w)⟩
  85
  86@[simp] theorem toComplex_zero : toComplex (0 : LogicComplex) = 0 := by
  87  exact toComplex_fromComplex 0
  88
  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. -/