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

phiInvSq_eq_two_minus_phi

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)

  60theorem phiInvSq_eq_two_minus_phi : 1 / phi^2 = 2 - phi := by

proof body

Tactic-mode proof.

  61  have hpos : phi^2 ≠ 0 := ne_of_gt (pow_pos phi_pos 2)
  62  have h2 : phi^2 = phi + 1 := phi_sq_eq
  63  have h3 : phi^3 = 2 * phi + 1 := phi_cubed_eq
  64  have hkey : phi^2 * (2 - phi) = 1 := by nlinarith [h2, h3]
  65  rw [eq_comm, eq_div_iff hpos]
  66  linarith [hkey]
  67
  68/-- 1/φ³ = 2φ - 3 (= the Cabibbo-angle factor). -/

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.