theorem proved term proof

`fromReal_toReal`

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

formal statement (Lean)

  82theorem fromReal_toReal (x : LogicReal) : fromReal (toReal x) = x := by

Term-mode proof.

  83  cases x
  84  simp [toReal, fromReal]
  85
  86/-- Carrier equivalence between recovered reals and Mathlib reals. -/

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

fromComplex_toComplex in IndisputableMonolith.Foundation.ComplexFromLogic decl_use
eq_iff_toReal_eq in IndisputableMonolith.Foundation.RealsFromLogic decl_use
equivReal in IndisputableMonolith.Foundation.RealsFromLogic decl_use
logicReal_recovered_from_completion in IndisputableMonolith.Foundation.RealsFromLogic decl_use

Lean names referenced from this declaration's body.