Theorems · Theorem · number theory

Polynomial.X_pow_sub_one_eq_prod

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R} {n : ℕ},
  0 < n →
    IsPrimitiveRoot ζ n → Polynomial.X ^ n - 1 = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (Polynomial.X - Polynomial.C ζ)

If there is a primitive nth root of unity in K, then X ^ n - 1 = ∏ (X - μ), where μ varies over the n-th roots of unity.

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomain