lemma proved term proof

`phi_minus_one_abs`

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

formal statement (Lean)

  92lemma phi_minus_one_abs : |Real.goldenRatio - 1| = Real.goldenRatio - 1 := by

Term-mode proof.

  93  rw [abs_of_pos phi_sub_one_pos]
  94
  95/-- x = φ - 1 satisfies |x| < 1 -/

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

phi_minus_one_abs_lt_one in IndisputableMonolith.Numerics.Interval.Log decl_use

Lean names referenced from this declaration's body.

phi_sub_one_pos in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use