Polynomial.cyclotomic_mul_prime_dvd_eq_pow
theorem Polynomial.cyclotomic_mul_prime_dvd_eq_pow :
∀ (R : Type u_1) {p n : ℕ} [hp : Fact p.Prime] [inst : Ring R] [inst_1 : CharP R p],
p ∣ n → Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n R ^ p
The theorem, `Polynomial.cyclotomic_mul_prime_dvd_eq_pow`, states that for any ring `R` with characteristic `p` and for any natural numbers `p` and `n` where `p` is a prime number and `p` divides `n`, the `n*p`-th cyclotomic polynomial over `R` is equal to the `n`-th cyclotomic polynomial over `R` raised to the power of `p`. In mathematical terms, if `R` has characteristic `p` and `p | n`, then `Cyclotomic(n*p, R) = (Cyclotomic(n, R))^p`.
More concisely: For a prime number `p` dividing natural number `n` in a ring `R` of characteristic `p`, the `n*p`-th cyclotomic polynomial equals the `n`-th cyclotomic polynomial raised to the power of `p`: `Cyclotomic(n*p, R) = (Cyclotomic(n, R))^p`.
|
Polynomial.cyclotomic_irreducible_of_irreducible_pow
theorem Polynomial.cyclotomic_irreducible_of_irreducible_pow :
∀ {p : ℕ},
p.Prime →
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ},
n ≠ 0 → Irreducible (Polynomial.cyclotomic (p ^ n) R) → Irreducible (Polynomial.cyclotomic p R)
The theorem `Polynomial.cyclotomic_irreducible_of_irreducible_pow` states that for any prime number `p` and any non-zero number `n`, if the `n`-th power of the `p` cyclotomic polynomial with coefficients in a domain `R` (where `R` is a commutative ring) is irreducible, then the `p` cyclotomic polynomial itself is also irreducible in `R`.
More concisely: If the `n`-th power of the `p`-th cyclotomic polynomial is irreducible in a commutative ring `R`, then the `p`-th cyclotomic polynomial is irreducible in `R`.
|
Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP
theorem Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP :
∀ {m k p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [hp : Fact p.Prime] [hchar : CharP R p]
{μ : R} [inst_2 : NeZero ↑m], (Polynomial.cyclotomic (p ^ k * m) R).IsRoot μ ↔ IsPrimitiveRoot μ m
The theorem `Polynomial.isRoot_cyclotomic_prime_pow_mul_iff_of_charP` states that for a given commutative ring `R` with characteristic `p`, and integers `m`, `k`, and `p` such that `p` is prime and does not divide `m`, then a number `μ` is a root of the cyclotomic polynomial `cyclotomic (p ^ k * m) R` if and only if `μ` is a primitive `m`-th root of unity. This unifies the behavior of cyclotomic polynomials and primitive roots of unity for a specific class of rings and inputs.
More concisely: For a commutative ring R with characteristic p, where p is prime and does not divide m, a number μ is a root of the cyclotomic polynomial cyclotomic (p^k * m) R if and only if μ is a primitive m-th root of unity.
|
Polynomial.cyclotomic_expand_eq_cyclotomic_mul
theorem Polynomial.cyclotomic_expand_eq_cyclotomic_mul :
∀ {p n : ℕ},
p.Prime →
¬p ∣ n →
∀ (R : Type u_1) [inst : CommRing R],
(Polynomial.expand R p) (Polynomial.cyclotomic n R) =
Polynomial.cyclotomic (n * p) R * Polynomial.cyclotomic n R
The theorem `Polynomial.cyclotomic_expand_eq_cyclotomic_mul` is about the relationship between the expansion and multiplication of cyclotomic polynomials. Specifically, if `p` is a prime number which does not divide `n`, then when we expand the `n`-th cyclotomic polynomial by a factor of `p` (so each term `aₙ xⁿ` becomes `aₙ xⁿᵖ`), it's equal to the product of the `n*p`-th cyclotomic polynomial and the `n`-th cyclotomic polynomial. This is true for any commutative ring `R`.
More concisely: For any prime number p not dividing n in a commutative ring R, the n-th cyclotomic polynomial expanded by a factor of p equals the product of the n*p-th and n-th cyclotomic polynomials.
|
Polynomial.cyclotomic_expand_eq_cyclotomic
theorem Polynomial.cyclotomic_expand_eq_cyclotomic :
∀ {p n : ℕ},
p.Prime →
p ∣ n →
∀ (R : Type u_1) [inst : CommRing R],
(Polynomial.expand R p) (Polynomial.cyclotomic n R) = Polynomial.cyclotomic (n * p) R
The theorem `Polynomial.cyclotomic_expand_eq_cyclotomic` states that for any prime number `p` and any natural number `n`, if `p` divides `n`, then expanding the `n`-th cyclotomic polynomial by a factor of `p` is equal to the `pn`-th cyclotomic polynomial, for any commutative ring `R`. In other words, if `p` is a prime divisor of `n`, the operation of expanding the `n`-th cyclotomic polynomial by `p` is equivalent to directly computing the `pn`-th cyclotomic polynomial in the ring `R`.
More concisely: For any prime number p and natural number n, the p-th power of the n-th cyclotomic polynomial is equal to the n-th cyclotomic polynomial of degree pn.
|
Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow
theorem Polynomial.cyclotomic_irreducible_pow_of_irreducible_pow :
∀ {p : ℕ},
p.Prime →
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {n m : ℕ},
m ≤ n → Irreducible (Polynomial.cyclotomic (p ^ n) R) → Irreducible (Polynomial.cyclotomic (p ^ m) R)
The theorem states that for any prime natural number `p`, and any two natural numbers `m` and `n` such that `m` is less than or equal to `n`, if the `p` to the power `n`th cyclotomic polynomial is irreducible in a commutative ring `R`, then the `p` to the power `m`th cyclotomic polynomial is also irreducible in the same ring `R`. In other words, irreducibility of a cyclotomic polynomial of a certain power of a prime carries over to all lower powers of that prime in a given commutative ring.
More concisely: For any prime number `p` and commutative ring `R`, if the `p`th cyclotomic polynomial raised to the power of `n` is irreducible in `R`, then the same holds for the `p`th cyclotomic polynomial raised to the power of `m`, where `m` is less than or equal to `n`.
|
Polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd
theorem Polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd :
∀ (R : Type u_1) {p n : ℕ} [hp : Fact p.Prime] [inst : Ring R] [inst_1 : CharP R p],
¬p ∣ n → Polynomial.cyclotomic (n * p) R = Polynomial.cyclotomic n R ^ (p - 1)
The theorem states that if `R` is a ring of characteristic `p`, where `p` is a prime number that does not divide `n`, then the `n*p`-th cyclotomic polynomial with coefficients in `R` is equal to the `n`-th cyclotomic polynomial raised to the power of `p - 1`.
More concisely: If `R` is a ring of characteristic `p` where `p` does not divide `n`, then the `n*p`-th cyclotomic polynomial in `R` equals the `n`-th cyclotomic polynomial raised to the power of `p-1`.
|
Polynomial.cyclotomic_mul_prime_pow_eq
theorem Polynomial.cyclotomic_mul_prime_pow_eq :
∀ (R : Type u_1) {p m : ℕ} [inst : Fact p.Prime] [inst : Ring R] [inst_1 : CharP R p],
¬p ∣ m →
∀ {k : ℕ}, 0 < k → Polynomial.cyclotomic (p ^ k * m) R = Polynomial.cyclotomic m R ^ (p ^ k - p ^ (k - 1))
The theorem `Polynomial.cyclotomic_mul_prime_pow_eq` states that if `R` is a ring of characteristic `p` (where `p` is a prime number) and `p` does not divide `m`, then for any positive integer `k`, the `p ^ k * m`-th cyclotomic polynomial with coefficients in `R` is equal to the `m`-th cyclotomic polynomial, raised to the power of `p ^ k - p ^ (k - 1)`. This theorem applies to any ring `R` and integers `p`, `m`, and `k`.
More concisely: For any prime number `p` not dividing `m`, and any positive integer `k`, the `p^k`-th cyclotomic polynomial with coefficients in a ring of characteristic `p` is equal to the `m`-th cyclotomic polynomial raised to the power of `p^k - p^(k-1)`.
|