# mathlib3documentation

ring_theory.polynomial.cyclotomic.expand

# Cyclotomic polynomials and expand. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We gather results relating cyclotomic polynomials and expand.

## Main results #

@[simp]
theorem polynomial.cyclotomic_expand_eq_cyclotomic_mul {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 (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.

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 : nat.prime p) {R : Type u_1} [comm_ring R] [is_domain R] {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 (nat.prime p)] [ring 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 (nat.prime p)] [ring 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] [ p] (hm : ¬p m) {k : } :
0 < k polynomial.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.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 : 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.