# Documentation

Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

# Cyclotomic polynomials and expand. #

We gather results relating cyclotomic polynomials and expand.

## Main results #

• Polynomial.cyclotomic_expand_eq_cyclotomic_mul : If p is a prime such that ¬ p ∣ n, then expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R).
• Polynomial.cyclotomic_expand_eq_cyclotomic : If p is a prime such that p ∣ n, then expand R p (cyclotomic n R) = cyclotomic (p * n) R.
• Polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd : If R is of characteristic p and ¬p ∣ n, then cyclotomic (n * p) R = (cyclotomic n R) ^ (p - 1).
• Polynomial.cyclotomic_mul_prime_dvd_eq_pow : If R is of characteristic p and p ∣ n, then cyclotomic (n * p) R = (cyclotomic n R) ^ p.
• Polynomial.cyclotomic_mul_prime_pow_eq : If R is of characteristic p and ¬p ∣ m, then cyclotomic (p ^ k * m) R = (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)).
@[simp]
theorem Polynomial.cyclotomic_expand_eq_cyclotomic_mul {p : } {n : } (hp : ) (hdiv : ¬p n) (R : Type u_1) [] :
↑() () = Polynomial.cyclotomic (n * p) R *

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 : ) (hdiv : p n) (R : Type u_1) [] :
↑() () = Polynomial.cyclotomic (n * p) 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 : ) {R : Type u_1} [] [] {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.

theorem Polynomial.cyclotomic_irreducible_of_irreducible_pow {p : } (hp : ) {R : Type u_1} [] [] {n : } (hn : n 0) (h : Irreducible (Polynomial.cyclotomic (p ^ n) R)) :

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 ()] [Ring R] [CharP R p] (hn : ¬p n) :
Polynomial.cyclotomic (n * p) R = ^ (p - 1)

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 ()] [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 ()] [Ring R] [CharP R p] (hm : ¬p m) {k : } :
0 < kPolynomial.cyclotomic (p ^ k * 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} [] [] [hp : Fact ()] [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.