feat(ring_theory/polynomial/eisenstein): add cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at (#12707)
feat(ring_theory/polynomial/eisenstein): add cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at (#12707)

We add `cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at`.

From flt-regular





leanprover-community/mathlib,leanprover-community/mathlib