Commit 2021-12-28 03:25 612a4766

feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic (#10974) We prove that, if p ∣ n, then expand R p (cyclotomic n R) = cyclotomic (p * n) R.

• depends on: #10965
• depends on: #10971