structure
definition
PhiInt
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Algebra.PhiRing on GitHub at line 123.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
140/-- The element φ itself: 0 + 1·φ -/
141def PhiInt.phi : PhiInt := ⟨0, 1⟩
142
143/-- Addition in ℤ[φ]: (a₁ + b₁φ) + (a₂ + b₂φ) = (a₁+a₂) + (b₁+b₂)φ -/
144def PhiInt.add (z w : PhiInt) : PhiInt := ⟨z.a + w.a, z.b + w.b⟩
145
146/-- Negation in ℤ[φ]: -(a + bφ) = (-a) + (-b)φ -/
147def PhiInt.neg (z : PhiInt) : PhiInt := ⟨-z.a, -z.b⟩
148
149/-- Multiplication in ℤ[φ]: uses φ² = φ + 1 to reduce.
150 (a₁ + b₁φ)(a₂ + b₂φ) = a₁a₂ + (a₁b₂ + a₂b₁)φ + b₁b₂φ²
151 = a₁a₂ + (a₁b₂ + a₂b₁)φ + b₁b₂(φ + 1)
152 = (a₁a₂ + b₁b₂) + (a₁b₂ + a₂b₁ + b₁b₂)φ -/
153def PhiInt.mul (z w : PhiInt) : PhiInt :=