theorem
proved
phi_inv
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Algebra.PhiRing on GitHub at line 109.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
106 unfold φ ψ; ring
107
108/-- **THEOREM: φ⁻¹ = φ − 1** -/
109theorem phi_inv : φ⁻¹ = φ - 1 := by
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φ. -/
123@[ext]
124structure PhiInt where
125 /-- The "rational" part -/
126 a : ℤ
127 /-- The "φ" part -/
128 b : ℤ
129deriving DecidableEq, Repr
130
131/-- Interpret a PhiInt as a real number: a + bφ -/
132noncomputable def PhiInt.toReal (z : PhiInt) : ℝ := z.a + z.b * φ
133
134/-- Zero element: 0 + 0·φ = 0 -/
135def PhiInt.zero : PhiInt := ⟨0, 0⟩
136
137/-- One element: 1 + 0·φ = 1 -/
138def PhiInt.one : PhiInt := ⟨1, 0⟩
139