Commit 2023-06-20 23:47 c511043c

View on Github →

feat: port RingTheory.Polynomial.Eisenstein.IsIntegral (#5302) Fix also some names in RingTheory.Polynomial.Eisenstein.Basic that are in the wrong namespace.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean

deleted theorem Polynomial.IsEisensteinAt.Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem

deleted theorem Polynomial.IsEisensteinAt.Polynomial.Monic.leadingCoeff_not_mem

added theorem Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem

added theorem Polynomial.Monic.leadingCoeff_not_mem

Created Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

added theorem cyclotomic_comp_x_add_one_isEisensteinAt

added theorem cyclotomic_prime_pow_comp_x_add_one_isEisensteinAt

added theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_is_eiseinstein_at

added theorem mem_adjoin_of_dvd_coeff_of_dvd_aeval

added theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at

added theorem mem_adjoin_of_smul_prime_smul_of_minpoly_is_eiseinstein_at