Documentation

Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Cyclotomic polynomials and expand. #

We gather results relating cyclotomic polynomials and expand.

Main results #

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

If p is a prime such that p ∣ n, then expand R p (cyclotomic n R) = 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] [CharP 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] [CharP 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] [CharP 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.isRoot_cyclotomic_prime_pow_mul_iff_of_charP {m : } {k : } {p : } {R : Type u_1} [CommRing R] [IsDomain R] [hp : Fact (Nat.Prime p)] [hchar : CharP R p] {μ : R} [NeZero 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.