Theorems · Theorem · number theory

Polynomial.cyclotomic_expand_eq_cyclotomic_mul

∀ {p n : ℕ},
  Nat.Prime p →
    ¬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

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

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Cited by

2 results in Mathlib

Foundations

Depth 212 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing