Commit 2023-04-12 19:26 5771d641

View on Github →

feat: port RingTheory.Polynomial.Eisenstein.Basic (#3382)

Estimated changes

Modified Mathlib.lean

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

added theorem Polynomial.IsEisensteinAt.Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem

added theorem Polynomial.IsEisensteinAt.Polynomial.Monic.leadingCoeff_not_mem

added theorem Polynomial.IsEisensteinAt.coeff_mem

added theorem Polynomial.IsEisensteinAt.irreducible

added theorem Polynomial.IsEisensteinAt.isWeaklyEisensteinAt

added structure Polynomial.IsEisensteinAt

added theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree

added theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le

added theorem Polynomial.IsWeaklyEisensteinAt.map

added theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map

added theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem

added structure Polynomial.IsWeaklyEisensteinAt

added theorem Polynomial.dvd_pow_natDegree_of_aeval_eq_zero

added theorem Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero

added theorem Polynomial.scaleRoots.isWeaklyEisensteinAt