Cyclotomic polynomials.

For n : ℕ and an integral domain R, we define a modified version of the n-th cyclotomic polynomial with coefficients in R, denoted cyclotomic' n R, as ∏ (X - μ), where μ varies over the primitive nth roots of unity. If there is a primitive nth root of unity in R then this the standard definition. We then define the standard cyclotomic polynomial cyclotomic n R with coefficients in any ring R.

Main definition

• cyclotomic n R : the n-th cyclotomic polynomial with coefficients in R.

Main results

• Polynomial.degree_cyclotomic : The degree of cyclotomic n is totient n.
• Polynomial.prod_cyclotomic_eq_X_pow_sub_one : X ^ n - 1 = ∏ (cyclotomic i), where i divides n.
• Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius : The Möbius inversion formula for cyclotomic n R over an abstract fraction field for R[X].

Implementation details

Our definition of cyclotomic' n R makes sense in any integral domain R, but the interesting results hold if there is a primitive n-th root of unity in R. In particular, our definition is not the standard one unless there is a primitive nth root of unity in R. For example, cyclotomic' 3 ℤ = 1, since there are no primitive cube roots of unity in ℤ. The main example is R = ℂ, we decided to work in general since the difficulties are essentially the same. To get the standard cyclotomic polynomials, we use unique_int_coeff_of_cycl, with R = ℂ, to get a polynomial with integer coefficients and then we map it to R[X], for any ring R.

def Polynomial.cyclotomic' (n : ℕ) (R : Type u_2) [CommRing R] [IsDomain R] : Polynomial R

The modified n-th cyclotomic polynomial with coefficients in R, it is the usual cyclotomic polynomial if there is a primitive n-th root of unity in R.

Equations

• Polynomial.cyclotomic' n R = ∏ μ ∈ primitiveRoots n R, (Polynomial.X - Polynomial.C μ)

@[simp]

theorem Polynomial.cyclotomic'_zero (R : Type u_2) [CommRing R] [IsDomain R] : cyclotomic' 0 R = 1

The zeroth modified cyclotomic polynomial is 1.

@[simp]

theorem Polynomial.cyclotomic'_one (R : Type u_2) [CommRing R] [IsDomain R] : cyclotomic' 1 R = X - 1

The first modified cyclotomic polynomial is X - 1.

theorem Polynomial.cyclotomic'_two (R : Type u_2) [CommRing R] [IsDomain R] (p : ℕ) [CharP R p] (hp : p ≠ 2) : cyclotomic' 2 R = X + 1

The second modified cyclotomic polynomial is X + 1 if the characteristic of R is not 2.

theorem Polynomial.cyclotomic'.monic (n : ℕ) (R : Type u_2) [CommRing R] [IsDomain R] : (cyclotomic' n R).Monic

cyclotomic' n R is monic.

theorem Polynomial.cyclotomic'_ne_zero (n : ℕ) (R : Type u_2) [CommRing R] [IsDomain R] : cyclotomic' n R ≠ 0

cyclotomic' n R is different from 0.

theorem Polynomial.natDegree_cyclotomic' {R : Type u_1} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (cyclotomic' n R).natDegree = n.totient

The natural degree of cyclotomic' n R is totient n if there is a primitive root of unity in R.

theorem Polynomial.degree_cyclotomic' {R : Type u_1} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) : (cyclotomic' n R).degree = ↑n.totient

The degree of cyclotomic' n R is totient n if there is a primitive root of unity in R.

theorem Polynomial.roots_of_cyclotomic (n : ℕ) (R : Type u_2) [CommRing R] [IsDomain R] : (cyclotomic' n R).roots = (primitiveRoots n R).val

The roots of cyclotomic' n R are the primitive n-th roots of unity.

theorem Polynomial.X_pow_sub_one_eq_prod {R : Type u_1} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : X ^ n - 1 = ∏ ζ ∈ nthRootsFinset n 1, (X - 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.

theorem Polynomial.cyclotomic'_splits {K : Type u_1} [Field K] (n : ℕ) : Splits (RingHom.id K) (cyclotomic' n K)

cyclotomic' n K splits.

theorem Polynomial.X_pow_sub_one_splits {K : Type u_1} [Field K] {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) : Splits (RingHom.id K) (X ^ n - C 1)

If there is a primitive n-th root of unity in K, then X ^ n - 1 splits.

theorem Polynomial.prod_cyclotomic'_eq_X_pow_sub_one {K : Type u_2} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : ∏ i ∈ n.divisors, cyclotomic' i K = X ^ n - 1

If there is a primitive n-th root of unity in K, then ∏ i ∈ Nat.divisors n, cyclotomic' i K = X ^ n - 1.

theorem Polynomial.cyclotomic'_eq_X_pow_sub_one_div {K : Type u_2} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : cyclotomic' n K = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic' i K

If there is a primitive n-th root of unity in K, then cyclotomic' n K = (X ^ k - 1) /ₘ (∏ i ∈ Nat.properDivisors k, cyclotomic' i K).

theorem Polynomial.int_coeff_of_cyclotomic' {K : Type u_2} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) : ∃ (P : Polynomial ℤ), map (Int.castRingHom K) P = cyclotomic' n K ∧ P.degree = (cyclotomic' n K).degree ∧ P.Monic

If there is a primitive n-th root of unity in K, then cyclotomic' n K comes from a monic polynomial with integer coefficients.

theorem Polynomial.unique_int_coeff_of_cycl {K : Type u_2} [CommRing K] [IsDomain K] [CharZero K] {ζ : K} {n : ℕ+} (h : IsPrimitiveRoot ζ ↑n) : ∃! P : Polynomial ℤ, map (Int.castRingHom K) P = cyclotomic' (↑n) K

If K is of characteristic 0 and there is a primitive n-th root of unity in K, then cyclotomic n K comes from a unique polynomial with integer coefficients.

def Polynomial.cyclotomic (n : ℕ) (R : Type u_1) [Ring R] : Polynomial R

The n-th cyclotomic polynomial with coefficients in R.

Equations

• Polynomial.cyclotomic n R = if h : n = 0 then 1 else Polynomial.map (Int.castRingHom R) ⋯.choose

theorem Polynomial.int_cyclotomic_rw {n : ℕ} (h : n ≠ 0) : cyclotomic n ℤ = ⋯.choose

theorem Polynomial.map_cyclotomic_int (n : ℕ) (R : Type u_1) [Ring R] : map (Int.castRingHom R) (cyclotomic n ℤ) = cyclotomic n R

cyclotomic n R comes from cyclotomic n ℤ.

theorem Polynomial.int_cyclotomic_spec (n : ℕ) : map (Int.castRingHom ℂ) (cyclotomic n ℤ) = cyclotomic' n ℂ ∧ (cyclotomic n ℤ).degree = (cyclotomic' n ℂ).degree ∧ (cyclotomic n ℤ).Monic

theorem Polynomial.int_cyclotomic_unique {n : ℕ} {P : Polynomial ℤ} (h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ) : P = cyclotomic n ℤ

@[simp]

theorem Polynomial.map_cyclotomic (n : ℕ) {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) : map f (cyclotomic n R) = cyclotomic n S

The definition of cyclotomic n R commutes with any ring homomorphism.

theorem Polynomial.cyclotomic.eval_apply {R : Type u_1} {S : Type u_2} (q : R) (n : ℕ) [Ring R] [Ring S] (f : R →+* S) : eval (f q) (cyclotomic n S) = f (eval q (cyclotomic n R))

@[simp]

theorem Polynomial.cyclotomic.eval_apply_ofReal (q : ℝ) (n : ℕ) : eval (↑q) (cyclotomic n ℂ) = ↑(eval q (cyclotomic n ℝ))

@[simp]

theorem Polynomial.cyclotomic_zero (R : Type u_1) [Ring R] : cyclotomic 0 R = 1

The zeroth cyclotomic polynomial is 1.

@[simp]

theorem Polynomial.cyclotomic_one (R : Type u_1) [Ring R] : cyclotomic 1 R = X - 1

The first cyclotomic polynomial is X - 1.

theorem Polynomial.cyclotomic.monic (n : ℕ) (R : Type u_1) [Ring R] : (cyclotomic n R).Monic

cyclotomic n is monic.

theorem Polynomial.cyclotomic.isPrimitive (n : ℕ) (R : Type u_1) [CommRing R] : (cyclotomic n R).IsPrimitive

cyclotomic n is primitive.

theorem Polynomial.cyclotomic_ne_zero (n : ℕ) (R : Type u_1) [Ring R] [Nontrivial R] : cyclotomic n R ≠ 0

cyclotomic n R is different from 0.

theorem Polynomial.degree_cyclotomic (n : ℕ) (R : Type u_1) [Ring R] [Nontrivial R] : (cyclotomic n R).degree = ↑n.totient

The degree of cyclotomic n is totient n.

theorem Polynomial.natDegree_cyclotomic (n : ℕ) (R : Type u_1) [Ring R] [Nontrivial R] : (cyclotomic n R).natDegree = n.totient

The natural degree of cyclotomic n is totient n.

theorem Polynomial.natDegree_cyclotomic_le {R : Type u_1} [Ring R] {n : ℕ} : (cyclotomic n R).natDegree ≤ n.totient

The natural degree of cyclotomic n is at most totient n.

If the base ring is nontrivial, then the degree is exactly φ n, otherwise it's zero.

theorem Polynomial.degree_cyclotomic_pos (n : ℕ) (R : Type u_1) (hpos : 0 < n) [Ring R] [Nontrivial R] : 0 < (cyclotomic n R).degree

The degree of cyclotomic n R is positive.

theorem Polynomial.prod_cyclotomic_eq_X_pow_sub_one {n : ℕ} (hpos : 0 < n) (R : Type u_1) [CommRing R] : ∏ i ∈ n.divisors, cyclotomic i R = X ^ n - 1

∏ i ∈ Nat.divisors n, cyclotomic i R = X ^ n - 1.

theorem Polynomial.cyclotomic.dvd_X_pow_sub_one (n : ℕ) (R : Type u_1) [Ring R] : cyclotomic n R ∣ X ^ n - 1

theorem Polynomial.prod_cyclotomic_eq_geom_sum {n : ℕ} (h : 0 < n) (R : Type u_1) [CommRing R] : ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ Finset.range n, X ^ i

theorem Polynomial.cyclotomic_prime (R : Type u_1) [Ring R] (p : ℕ) [hp : Fact (Nat.Prime p)] : cyclotomic p R = ∑ i ∈ Finset.range p, X ^ i

If p is prime, then cyclotomic p R = ∑ i ∈ range p, X ^ i.

theorem Polynomial.cyclotomic_prime_mul_X_sub_one (R : Type u_1) [Ring R] (p : ℕ) [hn : Fact (Nat.Prime p)] : cyclotomic p R * (X - 1) = X ^ p - 1

@[simp]

theorem Polynomial.cyclotomic_two (R : Type u_1) [Ring R] : cyclotomic 2 R = X + 1

@[simp]

theorem Polynomial.cyclotomic_three (R : Type u_1) [Ring R] : cyclotomic 3 R = X ^ 2 + X + 1

theorem Polynomial.cyclotomic_dvd_geom_sum_of_dvd (R : Type u_1) [Ring R] {d n : ℕ} (hdn : d ∣ n) (hd : d ≠ 1) : cyclotomic d R ∣ ∑ i ∈ Finset.range n, X ^ i

theorem Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd (R : Type u_1) [CommRing R] {d n : ℕ} (hdvd : d ∣ n) (hn : n ≠ 0) : (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

theorem Polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd (R : Type u_1) [CommRing R] {d n : ℕ} (h : d ∈ n.properDivisors) : (X ^ d - 1) * cyclotomic n R ∣ X ^ n - 1

theorem Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius {n : ℕ} (R : Type u_1) [CommRing R] [IsDomain R] : (algebraMap (Polynomial R) (RatFunc R)) (cyclotomic n R) = ∏ i ∈ n.divisorsAntidiagonal, (algebraMap (Polynomial R) (RatFunc R)) (X ^ i.2 - 1) ^ ArithmeticFunction.moebius i.1

cyclotomic n R can be expressed as a product in a fraction field of R[X] using Möbius inversion.

theorem Polynomial.cyclotomic_eq_X_pow_sub_one_div {R : Type u_1} [CommRing R] {n : ℕ} (hpos : 0 < n) : cyclotomic n R = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R

We have cyclotomic n R = (X ^ k - 1) /ₘ (∏ i ∈ Nat.properDivisors k, cyclotomic i K).

theorem Polynomial.X_pow_sub_one_dvd_prod_cyclotomic (R : Type u_1) [CommRing R] {n m : ℕ} (hpos : 0 < n) (hm : m ∣ n) (hdiff : m ≠ n) : X ^ m - 1 ∣ ∏ i ∈ n.properDivisors, cyclotomic i R

If m is a proper divisor of n, then X ^ m - 1 divides ∏ i ∈ Nat.properDivisors n, cyclotomic i R.

theorem Polynomial.cyclotomic_eq_prod_X_sub_primitiveRoots {K : Type u_1} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hz : IsPrimitiveRoot ζ n) : cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (X - C μ)

If there is a primitive n-th root of unity in K, then cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (X - C μ). ∈ particular, cyclotomic n K = cyclotomic' n K

theorem Polynomial.eq_cyclotomic_iff {R : Type u_1} [CommRing R] {n : ℕ} (hpos : 0 < n) (P : Polynomial R) : P = cyclotomic n R ↔ P * ∏ i ∈ n.properDivisors, cyclotomic i R = X ^ n - 1

theorem Polynomial.cyclotomic_prime_pow_eq_geom_sum {R : Type u_1} [CommRing R] {p n : ℕ} (hp : Nat.Prime p) : cyclotomic (p ^ (n + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ n) ^ i

If p ^ k is a prime power, then cyclotomic (p ^ (n + 1)) R = ∑ i ∈ range p, (X ^ (p ^ n)) ^ i.

theorem Polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type u_1) [CommRing R] (p k : ℕ) [hn : Fact (Nat.Prime p)] : cyclotomic (p ^ (k + 1)) R * (X ^ p ^ k - 1) = X ^ p ^ (k + 1) - 1

theorem Polynomial.cyclotomic_coeff_zero (R : Type u_1) [CommRing R] {n : ℕ} (hn : 1 < n) : (cyclotomic n R).coeff 0 = 1

The constant term of cyclotomic n R is 1 if 2 ≤ n.

theorem Polynomial.coprime_of_root_cyclotomic {n : ℕ} (hpos : 0 < n) {p : ℕ} [hprime : Fact (Nat.Prime p)] {a : ℕ} (hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)) : a.Coprime p

If (a : ℕ) is a root of cyclotomic n (ZMod p), where p is a prime, then a and p are coprime.

theorem Polynomial.orderOf_root_cyclotomic_dvd {n : ℕ} (hpos : 0 < n) {p : ℕ} [Fact (Nat.Prime p)] {a : ℕ} (hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)) : orderOf (ZMod.unitOfCoprime a ⋯) ∣ n

If (a : ℕ) is a root of cyclotomic n (ZMod p), then the multiplicative order of a modulo p divides n.

theorem Polynomial.dvd_C_mul_X_sub_one_pow_add_one {R : Type u_1} [CommRing R] {p : ℕ} (hpri : Nat.Prime p) (hp : p ≠ 2) (a r : R) (h₁ : r ∣ a ^ p) (h₂ : r ∣ ↑p * a) : C r ∣ (C a * X - 1) ^ p + 1

theorem IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul {R : Type u_1} [CommRing R] {ζ : R} {n : ℕ} (x y : R) [IsDomain R] (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) : x ^ n - y ^ n = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (x - ζ * y)

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

theorem IsPrimitiveRoot.pow_add_pow_eq_prod_add_mul {R : Type u_1} [CommRing R] {ζ : R} {n : ℕ} (x y : R) [IsDomain R] (hodd : Odd n) (h : IsPrimitiveRoot ζ n) : x ^ n + y ^ n = ∏ ζ ∈ Polynomial.nthRootsFinset n 1, (x + ζ * y)

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

theorem Polynomial.separable_cyclotomic (n : ℕ) (K : Type u_2) [Field K] [NeZero ↑n] : (cyclotomic n K).Separable

theorem Polynomial.squarefree_cyclotomic (n : ℕ) (K : Type u_2) [Field K] [NeZero ↑n] : Squarefree (cyclotomic n K)