2.6. n-th root of unity🔗

Definition 1.4.5. Given a positive integer n, a complex number \zeta is called an n-th root of unity if \zeta^n = 1.

/--
  Helper: if `z ^ n = ζ` and `ζ ≠ 0` and `n ≥ 1`,
  then `z ≠ 0`.
-/
lemma ne_zero_of_pow_eq_ne_zero (n : ℕ) (z ζ : ℂ)
   (hζ : ζ ≠ 0) (hn : n ≥ 1) (h : z ^ n = ζ) :
    z ≠ 0 := byn:ℕz:ℂζ:ℂhζ:ζ ≠ 0hn:n ≥ 1h:z ^ n = ζ⊢ z ≠ 0
  subst hn:ℕz:ℂhn:n ≥ 1hζ:z ^ n ≠ 0⊢ z ≠ 0
  simp_all only [ge_iff_le, ne_eq, pow_eq_zero_iff',
     not_and, Decidable.not_not]n:ℕz:ℂhn:1 ≤ nhζ:z = 0 → n = 0⊢ ¬z = 0
  intro hzn:ℕz:ℂhn:1 ≤ nhζ:z = 0 → n = 0hz:z = 0⊢ False ; subst hzn:ℕhn:1 ≤ nhζ:0 = 0 → n = 0⊢ False
  simp_all only [nonpos_iff_eq_zero, one_ne_zero]All goals completed! 🐙

/--
We prove that if `z₀` and `z₁` are both `n`-th roots
of a nonzero complex number `ζ`, then they differ by
 an `n`-th root of unity: there exists `ω` with
  `ω ^ n = 1` and `z₀ = z₁ * ω`.

Division by z₁ is well defined because z₁ is non-zero
by the previous helper lemma.
-/
example (n : ℕ) (z₀ z₁ ζ : ℂ) :
    n ≥ 1 → ζ ≠ 0 → z₀ ^ n = ζ → z₁ ^ n = ζ →
    ∃ ω : ℂ, z₀ = z₁ * ω ∧ ω ^ n = 1 := byn:ℕz₀:ℂz₁:ℂζ:ℂ⊢ n ≥ 1 → ζ ≠ 0 → z₀ ^ n = ζ → z₁ ^ n = ζ → ∃ ω, z₀ = z₁ * ω ∧ ω ^ n = 1
  intro hn hζn:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0⊢ z₀ ^ n = ζ → z₁ ^ n = ζ → ∃ ω, z₀ = z₁ * ω ∧ ω ^ n = 1 h₀n:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζ⊢ z₁ ^ n = ζ → ∃ ω, z₀ = z₁ * ω ∧ ω ^ n = 1 h₁n:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ ∃ ω, z₀ = z₁ * ω ∧ ω ^ n = 1
  use z₀/z₁hn:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ z₀ = z₁ * (z₀ / z₁) ∧ (z₀ / z₁) ^ n = 1
  constructorh.leftn:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ z₀ = z₁ * (z₀ / z₁)h.rightn:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ (z₀ / z₁) ^ n = 1
  ·h.leftn:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ z₀ = z₁ * (z₀ / z₁) rw [ mul_div_cancel₀ _ ?_]n:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ z₁ ≠ 0
    ·n:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ z₁ ≠ 0 rintro rfln:ℕz₀:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:0 ^ n = ζ⊢ False
      rw [ zero_pow ( by positivity ) ] at h₁n:ℕz₀:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:0 = ζ⊢ False
      subst h₀n:ℕz₀:ℂhn:n ≥ 1hζ:z₀ ^ n ≠ 0h₁:0 = z₀ ^ n⊢ False
      simp_all only [ge_iff_le, ne_eq, not_true_eq_false]All goals completed! 🐙
  ·h.rightn:ℕz₀:ℂz₁:ℂζ:ℂhn:n ≥ 1hζ:ζ ≠ 0h₀:z₀ ^ n = ζh₁:z₁ ^ n = ζ⊢ (z₀ / z₁) ^ n = 1 rw [ div_pow, h₀, h₁, div_self hζ ]All goals completed! 🐙

Example. Prove that

z = \frac{1}{4}(-1 + \sqrt{5} + i·\sqrt{10 + 2 \sqrt{5}})

is a 5-th root of unity. Fuerthermore, it is a root of the 5-th cyclotomic polynomial

z ^ 4 + z ^ 3 + z ^ 2 + z + 1 = 0.

section fifth_root_of_unity



open Real

-- define a complex number `z`
noncomputable def z : ℂ :=
  ⟨(-1 + Real.sqrt 5) / 4,
  Real.sqrt (10 + 2 * Real.sqrt 5) / 4⟩

-- Helper: (√5)² = 5
lemma sq_sqrt5 : Real.sqrt 5 ^ 2 = 5 := by⊢ √5 ^ 2 = 5
  rw [sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)]All goals completed! 🐙

-- Helper: (√(10 + 2√5))² = 10 + 2√5
lemma sq_sqrt_inner : Real.sqrt (10 + 2 * Real.sqrt 5) ^ 2
  = 10 + 2 * Real.sqrt 5 := by⊢ √(10 + 2 * √5) ^ 2 = 10 + 2 * √5
  rw [sq_sqrt]⊢ 0 ≤ 10 + 2 * √5
  linarith [Real.sqrt_nonneg 5]All goals completed! 🐙

/-- z satisfies the 5th cyclotomic polynomial -/
lemma z_cyclotomic :
  z ^ 4 + z ^ 3 + z ^ 2 + z + 1 = 0 := by⊢ z ^ 4 + z ^ 3 + z ^ 2 + z + 1 = 0
  refine' Complex.ext _ _refine'_1⊢ (z ^ 4 + z ^ 3 + z ^ 2 + z + 1).re = re 0refine'_2⊢ (z ^ 4 + z ^ 3 + z ^ 2 + z + 1).im = im 0;
  ·refine'_1⊢ (z ^ 4 + z ^ 3 + z ^ 2 + z + 1).re = re 0 unfold zrefine'_1⊢ ({ re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } ^ 4 + { re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } ^ 3 +
          { re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } ^ 2 +
        { re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } +
      1).re =
  re 0; norm_num [ pow_succ ]refine'_1⊢ (((-1 + √5) / 4 * ((-1 + √5) / 4) - √(10 + 2 * √5) / 4 * (√(10 + 2 * √5) / 4)) * ((-1 + √5) / 4) -
                ((-1 + √5) / 4 * (√(10 + 2 * √5) / 4) + √(10 + 2 * √5) / 4 * ((-1 + √5) / 4)) * (√(10 + 2 * √5) / 4)) *
              ((-1 + √5) / 4) -
            (((-1 + √5) / 4 * ((-1 + √5) / 4) - √(10 + 2 * √5) / 4 * (√(10 + 2 * √5) / 4)) * (√(10 + 2 * √5) / 4) +
                ((-1 + √5) / 4 * (√(10 + 2 * √5) / 4) + √(10 + 2 * √5) / 4 * ((-1 + √5) / 4)) * ((-1 + √5) / 4)) *
              (√(10 + 2 * √5) / 4) +
          (((-1 + √5) / 4 * ((-1 + √5) / 4) - √(10 + 2 * √5) / 4 * (√(10 + 2 * √5) / 4)) * ((-1 + √5) / 4) -
            ((-1 + √5) / 4 * (√(10 + 2 * √5) / 4) + √(10 + 2 * √5) / 4 * ((-1 + √5) / 4)) * (√(10 + 2 * √5) / 4)) +
        ((-1 + √5) / 4 * ((-1 + √5) / 4) - √(10 + 2 * √5) / 4 * (√(10 + 2 * √5) / 4)) +
      (-1 + √5) / 4 +
    1 =
  0 ; Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.ringrefine'_1⊢ 205 / 256 + √5 * (5 / 32) + √5 ^ 2 * (5 / 128) + √5 ^ 2 * √(10 + √5 * 2) ^ 2 * (-3 / 128) + √5 ^ 4 * (1 / 256) +
      √(10 + √5 * 2) ^ 2 * (-5 / 128) +
    √(10 + √5 * 2) ^ 4 * (1 / 256) =
  0;
    norm_numrefine'_1⊢ 205 / 256 + √5 * (5 / 32) + 25 / 128 + -(5 * √(10 + √5 * 2) ^ 2 * (3 / 128)) + √5 ^ 4 * (1 / 256) +
      -(√(10 + √5 * 2) ^ 2 * (5 / 128)) +
    √(10 + √5 * 2) ^ 4 * (1 / 256) =
  0;
    rw [ show Real.sqrt 5 ^ 4 =
       ( Real.sqrt 5 ^ 2 ) ^ 2 by ring,
         show Real.sqrt ( 10 + Real.sqrt 5 * 2 ) ^ 4
          = ( Real.sqrt ( 10 + Real.sqrt 5 * 2 ) ^ 2 ) ^ 2
          by ring, Real.sq_sqrt, Real.sq_sqrt ]refine'_1⊢ 205 / 256 + √5 * (5 / 32) + 25 / 128 + -(5 * (10 + √5 * 2) * (3 / 128)) + 5 ^ 2 * (1 / 256) +
      -((10 + √5 * 2) * (5 / 128)) +
    (10 + √5 * 2) ^ 2 * (1 / 256) =
  0refine'_1⊢ 0 ≤ 5refine'_1⊢ 0 ≤ 10 + √5 * 2 <;>refine'_1⊢ 205 / 256 + √5 * (5 / 32) + 25 / 128 + -(5 * (10 + √5 * 2) * (3 / 128)) + 5 ^ 2 * (1 / 256) +
      -((10 + √5 * 2) * (5 / 128)) +
    (10 + √5 * 2) ^ 2 * (1 / 256) =
  0refine'_1⊢ 0 ≤ 5refine'_1⊢ 0 ≤ 10 + √5 * 2
             nlinarith [ Real.sqrt_nonneg 5,
             Real.sq_sqrt ( show 0 ≤ 5 by⊢ z ^ 4 + z ^ 3 + z ^ 2 + z + 1 = 0 norm_numAll goals completed! 🐙 )];
  ·refine'_2⊢ (z ^ 4 + z ^ 3 + z ^ 2 + z + 1).im = im 0 unfold zrefine'_2⊢ ({ re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } ^ 4 + { re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } ^ 3 +
          { re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } ^ 2 +
        { re := (-1 + √5) / 4, im := √(10 + 2 * √5) / 4 } +
      1).im =
  im 0;
    norm_num [ pow_succ ]refine'_2⊢ (((-1 + √5) / 4 * ((-1 + √5) / 4) - √(10 + 2 * √5) / 4 * (√(10 + 2 * √5) / 4)) * ((-1 + √5) / 4) -
              ((-1 + √5) / 4 * (√(10 + 2 * √5) / 4) + √(10 + 2 * √5) / 4 * ((-1 + √5) / 4)) * (√(10 + 2 * √5) / 4)) *
            (√(10 + 2 * √5) / 4) +
          (((-1 + √5) / 4 * ((-1 + √5) / 4) - √(10 + 2 * √5) / 4 * (√(10 + 2 * √5) / 4)) * (√(10 + 2 * √5) / 4) +
              ((-1 + √5) / 4 * (√(10 + 2 * √5) / 4) + √(10 + 2 * √5) / 4 * ((-1 + √5) / 4)) * ((-1 + √5) / 4)) *
            ((-1 + √5) / 4) +
        (((-1 + √5) / 4 * ((-1 + √5) / 4) - √(10 + 2 * √5) / 4 * (√(10 + 2 * √5) / 4)) * (√(10 + 2 * √5) / 4) +
          ((-1 + √5) / 4 * (√(10 + 2 * √5) / 4) + √(10 + 2 * √5) / 4 * ((-1 + √5) / 4)) * ((-1 + √5) / 4)) +
      ((-1 + √5) / 4 * (√(10 + 2 * √5) / 4) + √(10 + 2 * √5) / 4 * ((-1 + √5) / 4)) +
    √(10 + 2 * √5) / 4 =
  0 ; ring_nfrefine'_2⊢ √5 * √(10 + √5 * 2) * (5 / 64) + √5 * √(10 + √5 * 2) ^ 3 * (-1 / 64) + √5 ^ 3 * √(10 + √5 * 2) * (1 / 64) +
    √(10 + √5 * 2) * (5 / 32) =
  0 ; norm_numrefine'_2⊢ √5 * √(10 + √5 * 2) * (5 / 64) + -(√5 * √(10 + √5 * 2) ^ 3 * (1 / 64)) + √5 ^ 3 * √(10 + √5 * 2) * (1 / 64) +
    √(10 + √5 * 2) * (5 / 32) =
  0;
    grindAll goals completed! 🐙


theorem z_pow_five : z ^ 5 = 1 := by⊢ z ^ 5 = 1
  have hcycl := z_cyclotomichcycl:z ^ 4 + z ^ 3 + z ^ 2 + z + 1 = 0⊢ z ^ 5 = 1
  have hfact : z ^ 5 - 1 =
    (z - 1) * (z ^ 4 + z ^ 3 + z ^ 2 + z + 1) := by⊢ z ^ 5 = 1 ringAll goals completed! 🐙
  have h : z ^ 5 - 1 = 0 := by⊢ z ^ 5 = 1 rw [hfact, hcycl, mul_zero]All goals completed! 🐙
  linear_combination hAll goals completed! 🐙

end fifth_root_of_unity