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 : Nat.Prime p) (hdiv : ¬p ∣ n) (R : Type u_1) [CommRing R] : (Polynomial.expand R p) (Polynomial.cyclotomic n R) = Polynomial.cyclotomic (n * p) R * Polynomial.cyclotomic n 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) [CommRing R] : (Polynomial.expand R p) (Polynomial.cyclotomic n R) = 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 : Nat.Prime p) {R : Type u_1} [CommRing R] [IsDomain R] {n m : ℕ} (hmn : m ≤ n) (h : Irreducible (Polynomial.cyclotomic (p ^ n) R)) : Irreducible (Polynomial.cyclotomic (p ^ m) 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} [CommRing R] [IsDomain R] {n : ℕ} (hn : n ≠ 0) (h : Irreducible (Polynomial.cyclotomic (p ^ n) R)) : Irreducible (Polynomial.cyclotomic p 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] [CharP R p] (hn : ¬p ∣ n) : Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n 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] [CharP R p] (hn : p ∣ n) : Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n R ^ p

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 < k → Polynomial.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] : (Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ 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.