14 unfold phi 15 have h5 : (0 : ℝ) ≤ 5 := by norm_num 16 have hsqrt : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5 17 field_simp 18 ring_nf 19 rw [hsqrt] 20 ring 21 22/-- φ = 1 + 1/φ: The fixed-point equation. 23 24 Proof: From φ² = φ + 1, divide by φ (which is positive) to get φ = 1 + 1/φ 25 NOTE: Also defined in PhiSupport/Lemmas.lean for use by that module. 26 Renamed here to avoid conflict. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.