Documentation

Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Eisenstein polynomials #

In this file we gather more miscellaneous results about Eisenstein polynomials

Main results #

theorem cyclotomic_comp_X_add_one_isEisensteinAt (p : ) [hp : Fact (Nat.Prime p)] :
((Polynomial.cyclotomic p ).comp (Polynomial.X + 1)).IsEisensteinAt (Submodule.span {p})
theorem cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt (p : ) [hp : Fact (Nat.Prime p)] (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} [CommRing R] [Field K] [Field L] [Algebra K L] [Algebra R L] [Algebra R K] [IsScalarTower R K L] [Algebra.IsSeparable K L] [IsDomain R] [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L} (hp : Prime p) (hBint : IsIntegral R B.gen) {z : L} {Q : Polynomial R} (hQ : (Polynomial.aeval B.gen) Q = p z) (hzint : IsIntegral R z) (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} [CommSemiring A] [CommRing B] [Algebra A B] [NoZeroSMulDivisors A B] {Q : Polynomial A} {p : A} {x : B} {z : B} (hp : p 0) (hQ : iFinset.range (Q.natDegree + 1), p Q.coeff i) (hz : (Polynomial.aeval x) Q = p z) :
theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {R : Type u} {K : Type v} {L : Type z} {p : R} [CommRing R] [Field K] [Field L] [Algebra K L] [Algebra R L] [Algebra R K] [IsScalarTower R K L] [Algebra.IsSeparable K L] [IsDomain R] [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L} (hp : Prime p) (hBint : IsIntegral R B.gen) {z : L} (hzint : IsIntegral R z) (hz : p z Algebra.adjoin R {B.gen}) (hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})) :
z Algebra.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 • z ∈ adjoin R {B.gen}, then z ∈ adjoin R {B.gen}.

theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt {R : Type u} {K : Type v} {L : Type z} {p : R} [CommRing R] [Field K] [Field L] [Algebra K L] [Algebra R L] [Algebra R K] [IsScalarTower R K L] [Algebra.IsSeparable K L] [IsDomain R] [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L} (hp : Prime p) (hBint : IsIntegral R B.gen) {n : } {z : L} (hzint : IsIntegral R z) (hz : p ^ n z Algebra.adjoin R {B.gen}) (hei : (minpoly R B.gen).IsEisensteinAt (Submodule.span R {p})) :
z Algebra.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.