  24noncomputable section
  25
  26/-- Complex numbers built over recovered reals. -/
  27structure LogicComplex where
  28  re : LogicReal
  29  im : LogicReal
  30
  31namespace LogicComplex
  32
  33/-- Transport a recovered complex number to Mathlib's complex line. -/
  34def toComplex (z : LogicComplex) : ℂ :=
  35  ⟨toReal z.re, toReal z.im⟩
  36
  37/-- Transport a Mathlib complex number to the recovered complex line. -/
  38def fromComplex (z : ℂ) : LogicComplex where
  39  re := fromReal z.re
  40  im := fromReal z.im
  41
  42@[simp] theorem toComplex_re (z : LogicComplex) :
  43    (toComplex z).re = toReal z.re := rfl
  44
  45@[simp] theorem toComplex_im (z : LogicComplex) :
  46    (toComplex z).im = toReal z.im := rfl
  47
  48@[simp] theorem toComplex_fromComplex (z : ℂ) :
  49    toComplex (fromComplex z) = z := by
  50  apply Complex.ext <;> simp [toComplex, fromComplex, toReal_fromReal]
  51
  52@[simp] theorem fromComplex_toComplex (z : LogicComplex) :
  53    fromComplex (toComplex z) = z := by
  54  cases z with
  55  | mk re im =>
  56    simp [toComplex, fromComplex, fromReal_toReal]
  57

papers checked against this theorem

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