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

phi_ne_zero

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)

  28lemma phi_ne_zero : Constants.phi ≠ 0 := by

proof body

Tactic-mode proof.

  29  -- goldenRatio = (1+√5)/2 ≠ 0
  30  have : Real.goldenRatio ≠ 0 := by
  31    have hpos : 0 < Real.goldenRatio := Real.goldenRatio_pos
  32    exact ne_of_gt hpos
  33  simpa [phi_def] using this
  34
  35/-- φ^2 = φ + 1 using the closed form. -/

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.