mathlib3

52841fbf - feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic_mul (#11005)

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