Documentation

Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

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 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 : Polynomial.IsEisensteinAt (minpoly R B.gen) (Submodule.span R {p})) :
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 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 : ∀ (i : ), i p ) (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 : Polynomial.IsEisensteinAt (minpoly R B.gen) (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.