pith. machine review for the scientific record. sign in
theorem proved term proof

phi_irrational

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  61theorem phi_irrational : Irrational phi := by

proof body

Term-mode proof.

  62  -- Our phi equals Mathlib's goldenRatio
  63  have h_eq : phi = Real.goldenRatio := rfl
  64  rw [h_eq]
  65  exact Real.goldenRatio_irrational
  66
  67/-! ### φ power bounds -/
  68
  69/-- Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0). -/

used by (6)

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

depends on (4)

Lean names referenced from this declaration's body.