mathlib

612a4766 - feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic (#10974)

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`. - [x] depends on: #10965 - [x] depends on: #10971