Commit 2022-03-26 23:17 f5a9d0a3

View on Github →

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

Estimated changes

Modified src/ring_theory/polynomial/eisenstein.lean

added theorem cyclotomic_prime_pow_comp_X_add_one_is_eisenstein_at

added theorem polynomial.monic.is_eisenstein_at_of_mem_of_not_mem

added theorem polynomial.monic.leading_coeff_not_mem