theorem proved wrapper

`toComplex_fromComplex`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  48@[simp] theorem toComplex_fromComplex (z : ℂ) :
  49    toComplex (fromComplex z) = z := by

One-line wrapper that applies apply.

  50  apply Complex.ext <;> simp [toComplex, fromComplex, toReal_fromReal]
  51

From the project-wide theorem graph. These declarations reference this one in their body.

equivComplex in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
logicComplex_recovered_from_mathlib in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_one in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
toComplex_zero in IndisputableMonolith.Foundation.ComplexFromLogic decl_use

Lean names referenced from this declaration's body.