mathlib documentation

ring_theory.polynomial.cyclotomic.basic

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 #

Main results #

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 int_coeff_of_cycl, with R = ℂ, to get a polynomial with integer coefficients and then we map it to polynomial R, for any ring R. To prove cyclotomic.irreducible, the irreducibility of cyclotomic n ℤ, we show in cyclotomic_eq_minpoly that cyclotomic n ℤ is the minimal polynomial of any n-th primitive root of unity μ : K, where K is a field of characteristic 0.

noncomputable def polynomial.cyclotomic' (n : ) (R : Type u_1) [comm_ring R] [is_domain 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
@[simp]
theorem polynomial.cyclotomic'_zero (R : Type u_1) [comm_ring R] [is_domain R] :

The zeroth modified cyclotomic polyomial is 1.

@[simp]

The first modified cyclotomic polyomial is X - 1.

@[simp]
theorem polynomial.cyclotomic'_two (R : Type u_1) [comm_ring R] [is_domain R] (p : ) [char_p R p] (hp : p 2) :

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

theorem polynomial.cyclotomic'.monic (n : ) (R : Type u_1) [comm_ring R] [is_domain R] :

cyclotomic' n R is monic.

theorem polynomial.cyclotomic'_ne_zero (n : ) (R : Type u_1) [comm_ring R] [is_domain R] :

cyclotomic' n R is different from 0.

theorem polynomial.nat_degree_cyclotomic' {R : Type u_1} [comm_ring R] [is_domain R] {ζ : R} {n : } (h : is_primitive_root ζ n) :

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} [comm_ring R] [is_domain R] {ζ : R} {n : } (h : is_primitive_root ζ n) :

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

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} [comm_ring R] [is_domain R] {ζ : R} {n : } (hpos : 0 < n) (h : is_primitive_root ζ n) :

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.

cyclotomic' n K splits.

theorem polynomial.X_pow_sub_one_splits {K : Type u_1} [field K] {ζ : K} {n : } (h : is_primitive_root ζ n) :

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

theorem polynomial.prod_cyclotomic'_eq_X_pow_sub_one {K : Type u_1} [comm_ring K] [is_domain K] {ζ : K} {n : } (hpos : 0 < n) (h : is_primitive_root ζ n) :

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

theorem polynomial.cyclotomic'_eq_X_pow_sub_one_div {K : Type u_1} [comm_ring K] [is_domain K] {ζ : K} {n : } (hpos : 0 < n) (h : is_primitive_root ζ n) :

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

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

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.

noncomputable def polynomial.cyclotomic (n : ) (R : Type u_1) [ring R] :

The n-th cyclotomic polynomial with coefficients in R.

Equations

cyclotomic n R comes from cyclotomic n ℤ.

@[simp]
theorem polynomial.map_cyclotomic (n : ) {R : Type u_1} {S : Type u_2} [ring R] [ring S] (f : R →+* 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) :
@[simp]
theorem polynomial.cyclotomic_zero (R : Type u_1) [ring R] :

The zeroth cyclotomic polyomial is 1.

@[simp]
theorem polynomial.cyclotomic_one (R : Type u_1) [ring R] :

The first cyclotomic polyomial is X - 1.

@[simp]
theorem polynomial.cyclotomic_two (R : Type u_1) [ring R] :

The second cyclotomic polyomial is X + 1.

theorem polynomial.cyclotomic.monic (n : ) (R : Type u_1) [ring R] :

cyclotomic n is monic.

cyclotomic n is primitive.

theorem polynomial.cyclotomic_ne_zero (n : ) (R : Type u_1) [ring R] [nontrivial R] :

cyclotomic n R is different from 0.

theorem polynomial.degree_cyclotomic (n : ) (R : Type u_1) [ring R] [nontrivial R] :

The degree of cyclotomic n is totient n.

The natural degree of cyclotomic n is totient n.

theorem polynomial.degree_cyclotomic_pos (n : ) (R : Type u_1) (hpos : 0 < n) [ring R] [nontrivial R] :

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) [comm_ring R] :

∏ i in nat.divisors n, cyclotomic i R = X ^ n - 1.

theorem polynomial.prod_cyclotomic_eq_geom_sum {n : } (h : 0 < n) (R : Type u_1) [comm_ring R] [is_domain R] :
(n.divisors \ {1}).prod (λ (i : ), polynomial.cyclotomic i R) = (finset.range n).sum (λ (i : ), polynomial.X ^ i)
theorem polynomial.cyclotomic_dvd_geom_sum_of_dvd (R : Type u_1) [comm_ring R] {d n : } (hdn : d n) (hd : d 1) :
theorem is_root_of_unity_iff {n : } (h : 0 < n) (R : Type u_1) [comm_ring R] [is_domain R] {ζ : R} :
ζ ^ n = 1 ∃ (i : ) (H : i n.divisors), (polynomial.cyclotomic i R).is_root ζ
theorem polynomial.is_root_of_unity_of_root_cyclotomic {n : } {R : Type u_1} [comm_ring R] {ζ : R} {i : } (hi : i n.divisors) (h : (polynomial.cyclotomic i R).is_root ζ) :
ζ ^ n = 1

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

theorem polynomial.cyclotomic_eq_X_pow_sub_one_div {R : Type u_1} [comm_ring R] {n : } (hpos : 0 < n) :

We have cyclotomic n R = (X ^ k - 1) /ₘ (∏ i in nat.proper_divisors k, cyclotomic i K).

theorem polynomial.X_pow_sub_one_dvd_prod_cyclotomic (R : Type u_1) [comm_ring R] {n m : } (hpos : 0 < n) (hm : m n) (hdiff : m n) :

If m is a proper divisor of n, then X ^ m - 1 divides ∏ i in nat.proper_divisors n, cyclotomic i R.

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

theorem is_primitive_root.is_root_cyclotomic {R : Type u_1} {n : } [comm_ring R] [is_domain R] (hpos : 0 < n) {μ : R} (h : is_primitive_root μ n) :

Any n-th primitive root of unity is a root of cyclotomic n K.

theorem polynomial.is_root_cyclotomic_iff_char_zero {n : } {R : Type u_1} [comm_ring R] [is_domain R] [char_zero R] {μ : R} (hn : 0 < n) :

If R is of characteristic zero, then ζ is a root of cyclotomic n R if and only if it is a primitive n-th root of unity.

Over a ring R of characteristic zero, λ n, cyclotomic n R is injective.

theorem polynomial.eq_cyclotomic_iff {R : Type u_1} [comm_ring R] {n : } (hpos : 0 < n) (P : polynomial R) :
theorem polynomial.cyclotomic_eq_geom_sum {R : Type u_1} [comm_ring R] {p : } (hp : nat.prime p) :

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

theorem polynomial.cyclotomic_prime_pow_eq_geom_sum {R : Type u_1} [comm_ring R] {p n : } (hp : nat.prime p) :
polynomial.cyclotomic (p ^ (n + 1)) R = (finset.range p).sum (λ (i : ), (polynomial.X ^ p ^ n) ^ i)

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

theorem polynomial.cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type u_1) [comm_ring R] (p k : ) [hn : fact (nat.prime p)] :
polynomial.cyclotomic (p ^ (k + 1)) R * (polynomial.X ^ p ^ k - 1) = polynomial.X ^ p ^ (k + 1) - 1
theorem polynomial.cyclotomic_coeff_zero (R : Type u_1) [comm_ring R] {n : } (hn : 2 n) :

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 : (polynomial.cyclotomic n (zmod p)).is_root ((nat.cast_ring_hom (zmod p)) a)) :

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

theorem polynomial.order_of_root_cyclotomic_dvd {n : } (hpos : 0 < n) {p : } [fact (nat.prime p)] {a : } (hroot : (polynomial.cyclotomic n (zmod p)).is_root ((nat.cast_ring_hom (zmod p)) a)) :

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

theorem is_primitive_root.minpoly_dvd_cyclotomic {n : } {K : Type u_1} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :

The minimal polynomial of a primitive n-th root of unity μ divides cyclotomic n ℤ.

theorem is_primitive_root.minpoly_eq_cyclotomic_of_irreducible {K : Type u_1} [field K] {R : Type u_2} [comm_ring R] [is_domain R] {μ : R} {n : } [algebra K R] (hμ : is_primitive_root μ n) (h : irreducible (polynomial.cyclotomic n K)) [ne_zero n] :
theorem polynomial.cyclotomic_eq_minpoly {n : } {K : Type u_1} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :

cyclotomic n ℤ is the minimal polynomial of a primitive n-th root of unity μ.

theorem polynomial.cyclotomic_eq_minpoly_rat {n : } {K : Type u_1} [field K] {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n) [char_zero K] :

cyclotomic n ℚ is the minimal polynomial of a primitive n-th root of unity μ.

cyclotomic n ℤ is irreducible.

cyclotomic n ℚ is irreducible.

If n ≠ m, then (cyclotomic n ℚ) and (cyclotomic m ℚ) are coprime.

@[simp]

If p is a prime such that ¬ p ∣ n, then expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R).

@[simp]
theorem polynomial.cyclotomic_expand_eq_cyclotomic {p n : } (hp : nat.prime p) (hdiv : p n) (R : Type u_1) [comm_ring R] :

If p is a prime such that p ∣ n, then expand R p (cyclotomic n R) = cyclotomic (p * n) R.

theorem polynomial.cyclotomic_irreducible_pow_of_irreducible_pow {p : } (hp : nat.prime p) {R : Type u_1} [comm_ring R] [is_domain R] {n m : } (hmn : m n) (h : irreducible (polynomial.cyclotomic (p ^ n) R)) :

If the p ^ nth cyclotomic polynomial is irreducible, so is the p ^ mth, for m ≤ n.

If irreducible (cyclotomic (p ^ n) R) then irreducible (cyclotomic p R).

theorem polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd (R : Type u_1) {p n : } [hp : fact (nat.prime p)] [ring R] [char_p R p] (hn : ¬p n) :

If R is of characteristic p and ¬p ∣ n, then cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1).

theorem polynomial.cyclotomic_mul_prime_dvd_eq_pow (R : Type u_1) {p n : } [hp : fact (nat.prime p)] [ring R] [char_p R p] (hn : p n) :

If R is of characteristic p and p ∣ n, then cyclotomic (n * p) R = (cyclotomic n R) ^ p.

theorem polynomial.cyclotomic_mul_prime_pow_eq (R : Type u_1) {p m : } [fact (nat.prime p)] [ring R] [char_p R p] (hm : ¬p m) {k : } :
0 < kpolynomial.cyclotomic (p ^ k * m) R = polynomial.cyclotomic m R ^ (p ^ k - p ^ (k - 1))

If R is of characteristic p and ¬p ∣ m, then cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)).

theorem polynomial.is_root_cyclotomic_prime_pow_mul_iff_of_char_p {m k p : } {R : Type u_1} [comm_ring R] [is_domain R] [hp : fact (nat.prime p)] [hchar : char_p R p] {μ : R} [ne_zero m] :

If R is of characteristic p and ¬p ∣ m, then ζ is a root of cyclotomic (p ^ k * m) R if and only if it is a primitive m-th root of unity.