lemma proved term proof

`one_add_inv_phi_eq_phi`

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

formal statement (Lean)

  56lemma one_add_inv_phi_eq_phi : 1 + (1 : ℝ) / phi = phi := by

Term-mode proof.

  57  simpa using phi_eq_one_add_inv_phi.symm
  58
  59/-- Log rewrite at the canonical shift argument. -/

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

log_one_add_inv_phi_eq_log_phi in IndisputableMonolith.Masses.GapFunctionForcing decl_use
log_one_add_inv_phi_eq_log_phi in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use
one_add_inv_phi_eq_phi in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use

Lean names referenced from this declaration's body.

canonical in IndisputableMonolith.Foundation.ArithmeticOf decl_use
canonical in IndisputableMonolith.Gap45.Beat decl_use
phi_eq_one_add_inv_phi in IndisputableMonolith.Masses.GapFunctionForcing decl_use
canonical in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
one_add_inv_phi_eq_phi in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use
phi_eq_one_add_inv_phi in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use