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

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

 153theorem phi_cubed_eq : phi ^ 3 = 2 * phi + 1 := by

proof body

Tactic-mode proof.

 154  have h : phi ^ 2 = phi + 1 := phi_sq_eq
 155  have h_step : phi ^ 3 = phi ^ 2 * phi := by ring
 156  rw [h_step, h]
 157  ring_nf
 158  rw [h]
 159  ring
 160
 161/-- The ratio is strictly above 4. -/

used by (20)

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

depends on (9)

Lean names referenced from this declaration's body.