pith. machine review for the scientific record. sign in
lemma proved tactic proof

phi_eighth_eq

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)

 185lemma phi_eighth_eq : phi^8 = 21 * phi + 13 := by

proof body

Tactic-mode proof.

 186  calc phi^8 = phi * phi^7 := by ring
 187    _ = phi * (13 * phi + 8) := by rw [phi_seventh_eq]
 188    _ = 13 * phi^2 + 8 * phi := by ring
 189    _ = 13 * (phi + 1) + 8 * phi := by rw [phi_sq_eq]
 190    _ = 21 * phi + 13 := by ring
 191
 192/-- Key identity: φ⁹ = 34φ + 21 (Fibonacci recurrence). -/

used by (4)

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

depends on (5)

Lean names referenced from this declaration's body.