mathlib

5bfbcca0 - chore(ring_theory.polynomial.cyclotomic): split file (#19077)

chore(ring_theory.polynomial.cyclotomic): split file (#19077) `ring_theory.polynomial.cyclotomic` is almost 1000 lines long and it can be nicely split. We also fix some docstring.