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

phi_inv

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)

 109theorem phi_inv : φ⁻¹ = φ - 1 := by

proof body

Tactic-mode proof.

 110  unfold φ
 111  have hden : ((1 + Real.sqrt 5) / 2 : ℝ) ≠ 0 := by
 112    have hφ : 0 < ((1 + Real.sqrt 5) / 2 : ℝ) := by
 113      have h := sqrt5_pos
 114      linarith
 115    exact ne_of_gt hφ
 116  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)
 117  field_simp [hden]
 118  nlinarith [h5]
 119
 120/-! ## §2. Elements of ℤ[φ] -/
 121
 122/-- An element of ℤ[φ] is a pair (a, b) representing a + bφ. -/

used by (15)

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

depends on (13)

Lean names referenced from this declaration's body.