# Eisenstein polynomials #

In this file we gather more miscellaneous results about Eisenstein polynomials

## Main results #

• mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt: let K be the field of fraction of an integrally closed domain R and let L be a separable extension of K, generated by an integral power basis B such that the minimal polynomial of B.gen is Eisenstein at p. Given z : L integral over R, if p ^ n • z ∈ adjoin R {B.gen}, then z ∈ adjoin R {B.gen}. Together with Algebra.discr_mul_isIntegral_mem_adjoin this result often allows to compute the ring of integers of L.
theorem cyclotomic_comp_X_add_one_isEisensteinAt (p : ) [hp : Fact p.Prime] :
(.comp (Polynomial.X + 1)).IsEisensteinAt (Submodule.span {p})
theorem cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt (p : ) [hp : Fact p.Prime] (n : ) :
((Polynomial.cyclotomic (p ^ (n + 1)) ).comp (Polynomial.X + 1)).IsEisensteinAt (Submodule.span {p})
theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt {R : Type u} {K : Type v} {L : Type z} {p : R} [] [] [] [Algebra K L] [Algebra R L] [Algebra R K] [] [] [] [] {B : } (hp : ) (hBint : IsIntegral R B.gen) {z : L} {Q : } (hQ : (Polynomial.aeval B.gen) Q = p z) (hzint : ) (hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})) :
p Q.coeff 0

Let K be the field of fraction of an integrally closed domain R and let L be a separable extension of K, generated by an integral power basis B such that the minimal polynomial of B.gen is Eisenstein at p. Given z : L integral over R, if Q : R[X] is such that aeval B.gen Q = p • z, then p ∣ Q.coeff 0.

theorem mem_adjoin_of_dvd_coeff_of_dvd_aeval {A : Type u_1} {B : Type u_2} [] [] [Algebra A B] [] {Q : } {p : A} {x : B} {z : B} (hp : p 0) (hQ : iFinset.range (Q.natDegree + 1), p Q.coeff i) (hz : () Q = p z) :
theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {R : Type u} {K : Type v} {L : Type z} {p : R} [] [] [] [Algebra K L] [Algebra R L] [Algebra R K] [] [] [] [] {B : } (hp : ) (hBint : IsIntegral R B.gen) {z : L} (hzint : ) (hz : p z Algebra.adjoin R {B.gen}) (hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})) :
Let K be the field of fraction of an integrally closed domain R and let L be a separable extension of K, generated by an integral power basis B such that the minimal polynomial of B.gen is Eisenstein at p. Given z : L integral over R, if p • z ∈ adjoin R {B.gen}, then z ∈ adjoin R {B.gen}.
Let K be the field of fraction of an integrally closed domain R and let L be a separable extension of K, generated by an integral power basis B such that the minimal polynomial of B.gen is Eisenstein at p. Given z : L integral over R, if p ^ n • z ∈ adjoin R {B.gen}, then z ∈ adjoin R {B.gen}. Together with Algebra.discr_mul_isIntegral_mem_adjoin this result often allows to compute the ring of integers of L.