# mathlibdocumentation

ring_theory.polynomial.eisenstein

# Eisenstein polynomials #

Given an ideal 𝓟 of a commutative semiring R, we say that a polynomial f : R[X] is Eisenstein at 𝓟 if f.leading_coeff ∉ 𝓟, ∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟 and f.coeff 0 ∉ 𝓟 ^ 2. In this file we gather miscellaneous results about Eisenstein polynomials.

## Main definitions #

• polynomial.is_eisenstein_at f 𝓟: the property of being Eisenstein at 𝓟.

## Main results #

• polynomial.is_eisenstein_at.irreducible: if a primitive f satisfies f.is_eisenstein_at 𝓟, where 𝓟.is_prime, then f is irreducible.
• mem_adjoin_of_smul_prime_pow_smul_of_minpoly_is_eiseinstein_at: 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_is_integral_mem_adjoin this result often allows to compute the ring of integers of L.

## Implementation details #

We also define a notion is_weakly_eisenstein_at requiring only that ∀ n < f.nat_degree → f.coeff n ∈ 𝓟. This makes certain results slightly more general and it is useful since it is sometimes better behaved (for example it is stable under polynomial.map).

theorem polynomial.is_weakly_eisenstein_at_iff {R : Type u} (f : polynomial R) (𝓟 : ideal R) :
∀ {n : }, n < f.nat_degreef.coeff n 𝓟
structure polynomial.is_weakly_eisenstein_at {R : Type u} (f : polynomial R) (𝓟 : ideal R) :
Prop

Given an ideal 𝓟 of a commutative semiring R, we say that a polynomial f : R[X] is weakly Eisenstein at 𝓟 if ∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟.

structure polynomial.is_eisenstein_at {R : Type u} (f : polynomial R) (𝓟 : ideal R) :
Prop

Given an ideal 𝓟 of a commutative semiring R, we say that a polynomial f : R[X] is Eisenstein at 𝓟 if f.leading_coeff ∉ 𝓟, ∀ n, n < f.nat_degree → f.coeff n ∈ 𝓟 and f.coeff 0 ∉ 𝓟 ^ 2.

theorem polynomial.is_eisenstein_at_iff {R : Type u} (f : polynomial R) (𝓟 : ideal R) :
(∀ {n : }, n < f.nat_degreef.coeff n 𝓟) f.coeff 0 𝓟 ^ 2
theorem polynomial.is_weakly_eisenstein_at.map {R : Type u} {𝓟 : ideal R} {f : polynomial R} (hf : f.is_weakly_eisenstein_at 𝓟) {A : Type v} [comm_ring A] (φ : R →+* A) :
𝓟)
theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree {R : Type u} [comm_ring R] {f : polynomial R} {S : Type v} [comm_ring S] [ S] {p : R} {x : S} (hx : f = 0) (hmo : f.monic) (hf : f.is_weakly_eisenstein_at {p})) :
∃ (y : S) (H : y {x}), S) p * y = x ^ (polynomial.map S) f).nat_degree
theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le {R : Type u} [comm_ring R] {f : polynomial R} {S : Type v} [comm_ring S] [ S] {p : R} {x : S} (hx : f = 0) (hmo : f.monic) (hf : f.is_weakly_eisenstein_at {p})) (i : ) :
(polynomial.map S) f).nat_degree i(∃ (y : S) (H : y {x}), S) p * y = x ^ i)
theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_root_of_monic_mem {R : Type u} [comm_ring R] {𝓟 : ideal R} {f : polynomial R} (hf : f.is_weakly_eisenstein_at 𝓟) {x : R} (hroot : f.is_root x) (hmo : f.monic) (i : ) :
f.nat_degree ix ^ i 𝓟
theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_aeval_zero_of_monic_mem_map {R : Type u} [comm_ring R] {𝓟 : ideal R} {f : polynomial R} (hf : f.is_weakly_eisenstein_at 𝓟) {S : Type v} [comm_ring S] [ S] {x : S} (hx : f = 0) (hmo : f.monic) (i : ) :
(polynomial.map S) f).nat_degree ix ^ i ideal.map S) 𝓟
theorem polynomial.monic.leading_coeff_not_mem {R : Type u} {𝓟 : ideal R} {f : polynomial R} (hf : f.monic) (h : 𝓟 ) :
theorem polynomial.monic.is_eisenstein_at_of_mem_of_not_mem {R : Type u} {𝓟 : ideal R} {f : polynomial R} (hf : f.monic) (h : 𝓟 ) (hmem : ∀ {n : }, n < f.nat_degreef.coeff n 𝓟) (hnot_mem : f.coeff 0 𝓟 ^ 2) :
theorem polynomial.is_eisenstein_at.is_weakly_eisenstein_at {R : Type u} {𝓟 : ideal R} {f : polynomial R} (hf : f.is_eisenstein_at 𝓟) :
theorem polynomial.is_eisenstein_at.coeff_mem {R : Type u} {𝓟 : ideal R} {f : polynomial R} (hf : f.is_eisenstein_at 𝓟) {n : } (hn : n f.nat_degree) :
f.coeff n 𝓟
theorem polynomial.is_eisenstein_at.irreducible {R : Type u} [comm_ring R] [is_domain R] {𝓟 : ideal R} {f : polynomial R} (hf : f.is_eisenstein_at 𝓟) (hprime : 𝓟.is_prime) (hu : f.is_primitive) (hfd0 : 0 < f.nat_degree) :

If a primitive f satisfies f.is_eisenstein_at 𝓟, where 𝓟.is_prime, then f is irreducible.

theorem dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [ L] [ L] [ K] [ L] [ L] [is_domain R] [ K] {B : L} (hp : prime p) (hBint : B.gen) {z : L} {Q : polynomial R} (hQ : Q = p z) (hzint : z) (hei : (minpoly R B.gen).is_eisenstein_at {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 : polynomial R 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} [comm_ring B] [ B] {Q : polynomial A} {p : A} {x z : B} (hp : p 0) (hQ : ∀ (i : ), i finset.range (Q.nat_degree + 1)p Q.coeff i) (hz : Q = p z) :
z {x}
theorem mem_adjoin_of_smul_prime_smul_of_minpoly_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [ L] [ L] [ K] [ L] [ L] [is_domain R] [ K] {B : L} (hp : prime p) (hBint : B.gen) {z : L} (hzint : z) (hz : p z {B.gen}) (hei : (minpoly R B.gen).is_eisenstein_at {p})) :
z {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_is_eiseinstein_at {R : Type u} {K : Type v} {L : Type z} {p : R} [comm_ring R] [field K] [field L] [ L] [ L] [ K] [ L] [ L] [is_domain R] [ K] {B : L} (hp : prime p) (hBint : B.gen) {n : } {z : L} (hzint : z) (hz : p ^ n z {B.gen}) (hei : (minpoly R B.gen).is_eisenstein_at {p})) :
z {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_is_integral_mem_adjoin this result often allows to compute the ring of integers of L.