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

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

  81theorem phi_sq_eq : phi ^ 2 = phi + 1 := by

proof body

Tactic-mode proof.

  82  unfold phi
  83  have h5 : Real.sqrt 5 * Real.sqrt 5 = 5 :=
  84    Real.mul_self_sqrt (by norm_num : (5 : ℝ) ≥ 0)
  85  have : ((1 + Real.sqrt 5) / 2) ^ 2 = (1 + Real.sqrt 5) / 2 + 1 := by
  86    field_simp
  87    nlinarith [h5]
  88  exact this
  89
  90/-- `φ · φ⁻¹ = 1`. -/

used by (40)

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

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.