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 #

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)).
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 : 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.

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.

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] [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 : ℕ} :

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.