Commit 2021-12-30 14:14 52841fbf

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

• depends on: #10965