  56    simp [toComplex, fromComplex, fromReal_toReal]
  57
  58/-- Carrier equivalence between recovered complex numbers and Mathlib `ℂ`. -/
  59def equivComplex : LogicComplex ≃ ℂ where
  60  toFun := toComplex
  61  invFun := fromComplex
  62  left_inv := fromComplex_toComplex
  63  right_inv := toComplex_fromComplex
  64
  65/-- Equality transfer for recovered complex numbers. -/
  66theorem eq_iff_toComplex_eq {z w : LogicComplex} :
  67    z = w ↔ toComplex z = toComplex w := by
  68  constructor
  69  · exact congrArg toComplex
  70  · intro h
  71    have := congrArg fromComplex h
  72    rw [fromComplex_toComplex, fromComplex_toComplex] at this
  73    exact this
  74
  75/-! ## Algebra and coordinate transport -/
  76
  77instance : Zero LogicComplex := ⟨fromComplex 0⟩
  78instance : One LogicComplex := ⟨fromComplex 1⟩
  79instance : Add LogicComplex := ⟨fun z w => fromComplex (toComplex z + toComplex w)⟩
  80instance : Neg LogicComplex := ⟨fun z => fromComplex (-toComplex z)⟩
  81instance : Sub LogicComplex := ⟨fun z w => fromComplex (toComplex z - toComplex w)⟩
  82instance : Mul LogicComplex := ⟨fun z w => fromComplex (toComplex z * toComplex w)⟩
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.