Documentation

Mathlib.RingTheory.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 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.

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
Instances For
    @[simp]

    The zeroth modified cyclotomic polyomial is 1.

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

    The first modified cyclotomic polyomial is X - 1.

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

    The second modified cyclotomic polyomial 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 is monic.

    cyclotomic' n R is different from 0.

    theorem Polynomial.natDegree_cyclotomic' {R : Type u_1} [CommRing R] [IsDomain R] {ζ : R} {n : } (h : IsPrimitiveRoot ζ n) :
    (Polynomial.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) :
    (Polynomial.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] :

    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) :
    Polynomial.X ^ n - 1 = ζPolynomial.nthRootsFinset n R, (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.

    theorem Polynomial.X_pow_sub_one_splits {K : Type u_1} [Field K] {ζ : K} {n : } (h : IsPrimitiveRoot ζ n) :
    Polynomial.Splits (RingHom.id K) (Polynomial.X ^ n - Polynomial.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) :
    in.divisors, Polynomial.cyclotomic' i K = Polynomial.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) :
    Polynomial.cyclotomic' n K = (Polynomial.X ^ n - 1) /ₘ in.properDivisors, Polynomial.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) :

    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.

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

    The n-th cyclotomic polynomial with coefficients in R.

    Equations
    Instances For
      @[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]

      The zeroth cyclotomic polyomial is 1.

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

      The first cyclotomic polyomial is X - 1.

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

      cyclotomic n is monic.

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

      cyclotomic n is primitive.

      cyclotomic n R is different from 0.

      theorem Polynomial.degree_cyclotomic (n : ) (R : Type u_1) [Ring R] [Nontrivial R] :
      (Polynomial.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] :
      (Polynomial.cyclotomic n R).natDegree = n.totient

      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] :
      0 < (Polynomial.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] :
      in.divisors, Polynomial.cyclotomic i R = Polynomial.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] :
      Polynomial.cyclotomic n R Polynomial.X ^ n - 1
      theorem Polynomial.prod_cyclotomic_eq_geom_sum {n : } (h : 0 < n) (R : Type u_1) [CommRing R] :
      in.divisors.erase 1, Polynomial.cyclotomic i R = iFinset.range n, Polynomial.X ^ i
      theorem Polynomial.cyclotomic_prime (R : Type u_1) [Ring R] (p : ) [hp : Fact (Nat.Prime p)] :
      Polynomial.cyclotomic p R = iFinset.range p, Polynomial.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)] :
      Polynomial.cyclotomic p R * (Polynomial.X - 1) = Polynomial.X ^ p - 1
      @[simp]
      theorem Polynomial.cyclotomic_two (R : Type u_1) [Ring R] :
      Polynomial.cyclotomic 2 R = Polynomial.X + 1
      @[simp]
      theorem Polynomial.cyclotomic_three (R : Type u_1) [Ring R] :
      Polynomial.cyclotomic 3 R = Polynomial.X ^ 2 + Polynomial.X + 1
      theorem Polynomial.cyclotomic_dvd_geom_sum_of_dvd (R : Type u_1) [Ring R] {d : } {n : } (hdn : d n) (hd : d 1) :
      Polynomial.cyclotomic d R iFinset.range n, Polynomial.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 : } (h : d n.properDivisors) :
      (Polynomial.X ^ d - 1) * xn.divisors \ d.divisors, Polynomial.cyclotomic x R = Polynomial.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) :
      (Polynomial.X ^ d - 1) * Polynomial.cyclotomic n R Polynomial.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)) (Polynomial.cyclotomic n R) = in.divisorsAntidiagonal, (algebraMap (Polynomial R) (RatFunc R)) (Polynomial.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) :
      Polynomial.cyclotomic n R = (Polynomial.X ^ n - 1) /ₘ in.properDivisors, Polynomial.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) :
      Polynomial.X ^ m - 1 in.properDivisors, Polynomial.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) :
      Polynomial.cyclotomic n K = μprimitiveRoots n K, (Polynomial.X - Polynomial.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 = Polynomial.cyclotomic n R P * in.properDivisors, Polynomial.cyclotomic i R = Polynomial.X ^ n - 1
      theorem Polynomial.cyclotomic_prime_pow_eq_geom_sum {R : Type u_1} [CommRing R] {p : } {n : } (hp : Nat.Prime p) :
      Polynomial.cyclotomic (p ^ (n + 1)) R = iFinset.range p, (Polynomial.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)] :
      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) [CommRing R] {n : } (hn : 1 < n) :
      (Polynomial.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 : (Polynomial.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 : (Polynomial.cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)) :

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