mathlib3

c0ba4d69 - feat(ring_theory/polynomial/eisenstein): add cyclotomic_comp_X_add_one_is_eisenstein_at (#12447)

feat(ring_theory/polynomial/eisenstein): add cyclotomic_comp_X_add_one_is_eisenstein_at (#12447) We add `cyclotomic_comp_X_add_one_is_eisenstein_at`: `(cyclotomic p ℤ).comp (X + 1)` is Eisenstein at `p`. From flt-regular