mathlib3 documentation

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]

If p is a prime such that ¬ p ∣ n, then expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R).

@[simp]

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