phi_psi_product

formal source

  91  nlinarith [h5]
  92
  93/-- **THEOREM: φ · ψ = −1** (product of conjugates). -/
  94theorem phi_psi_product : φ * ψ = -1 := by
  95  unfold φ ψ
  96  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  97  ring_nf
  98  nlinarith [h5]
  99
 100/-- **THEOREM: φ + ψ = 1** (trace). -/
 101theorem phi_psi_sum : φ + ψ = 1 := by
 102  unfold φ ψ; ring
 103
 104/-- **THEOREM: φ − ψ = √5** -/
 105theorem phi_psi_diff : φ - ψ = Real.sqrt 5 := by
 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