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

phi_eleventh_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)

 209lemma phi_eleventh_eq : phi^11 = 89 * phi + 55 := by

proof body

Tactic-mode proof.

 210  calc phi^11 = phi * phi^10 := by ring
 211    _ = phi * (55 * phi + 34) := by rw [phi_tenth_eq]
 212    _ = 55 * phi^2 + 34 * phi := by ring
 213    _ = 55 * (phi + 1) + 34 * phi := by rw [phi_sq_eq]
 214    _ = 89 * phi + 55 := by ring
 215
 216/-! ### Canonical constants derived from φ -/
 217
 218/-- Canonical locked fine-structure constant: α_lock = (1 − 1/φ)/2. -/

used by (1)

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.