Theorems · Theorem · number theory

Polynomial.cyclotomic_expand_eq_cyclotomic

∀ {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

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

Defined in

Mathlib.RingTheory.Polynomial.Cyclotomic.Expand

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRing