# Documentation

Mathlib.RingTheory.Polynomial.Eisenstein.Basic

# Eisenstein polynomials #

Given an ideal π of a commutative semiring R, we say that a polynomial f : R[X] is Eisenstein at π if f.leadingCoeff β π, β n, n < f.natDegree β f.coeff n β π and f.coeff 0 β π ^ 2. In this file we gather miscellaneous results about Eisenstein polynomials.

## Main definitions #

• Polynomial.IsEisensteinAt f π: the property of being Eisenstein at π.

## Main results #

• Polynomial.IsEisensteinAt.irreducible: if a primitive f satisfies f.IsEisensteinAt π, where π.IsPrime, then f is irreducible.

## Implementation details #

We also define a notion IsWeaklyEisensteinAt requiring only that β n < f.natDegree β 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.IsWeaklyEisensteinAt_iff {R : Type u} [] (f : ) (π : ) :
β β {n : β}, β β π
structure Polynomial.IsWeaklyEisensteinAt {R : Type u} [] (f : ) (π : ) :

Given an ideal π of a commutative semiring R, we say that a polynomial f : R[X] is weakly Eisenstein at π if β n, n < f.natDegree β f.coeff n β π.

Instances For
theorem Polynomial.IsEisensteinAt_iff {R : Type u} [] (f : ) (π : ) :
β Β¬ β§ (β {n : β}, β β π) β§ Β¬ β π ^ 2
structure Polynomial.IsEisensteinAt {R : Type u} [] (f : ) (π : ) :

Given an ideal π of a commutative semiring R, we say that a polynomial f : R[X] is Eisenstein at π if f.leadingCoeff β π, β n, n < f.natDegree β f.coeff n β π and f.coeff 0 β π ^ 2.

Instances For
theorem Polynomial.IsWeaklyEisensteinAt.map {R : Type u} [] {π : } {f : } (hf : ) {A : Type v} [] (Ο : R β+* A) :
theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree {R : Type u} [] {f : } {S : Type v} [] [Algebra R S] {p : R} {x : S} (hx : β() f = 0) (hmo : ) (hf : ) :
β y, y β Algebra.adjoin R {x} β§ β() p * y = x ^ Polynomial.natDegree (Polynomial.map () f)
theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le {R : Type u} [] {f : } {S : Type v} [] [Algebra R S] {p : R} {x : S} (hx : β() f = 0) (hmo : ) (hf : ) (i : β) :
Polynomial.natDegree (Polynomial.map () f) β€ i β β y, y β Algebra.adjoin R {x} β§ β() p * y = x ^ i
theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem {R : Type u} [] {π : } {f : } (hf : ) {x : R} (hroot : ) (hmo : ) (i : β) :
β x ^ i β π
theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map {R : Type u} [] {π : } {f : } (hf : ) {S : Type v} [] [Algebra R S] {x : S} (hx : β() f = 0) (hmo : ) (i : β) :
theorem Polynomial.scaleRoots.isWeaklyEisensteinAt {R : Type u} [] (p : ) {x : R} {P : } (hP : x β P) :
theorem Polynomial.dvd_pow_natDegree_of_evalβ_eq_zero {R : Type u} {A : Type u_1} [] [] {f : R β+* A} (hf : ) {p : } (hp : ) (x : R) (y : R) (z : A) (h : = 0) (hz : βf x * z = βf y) :
theorem Polynomial.dvd_pow_natDegree_of_aeval_eq_zero {R : Type u} {A : Type u_1} [] [] [Algebra R A] [] [] {p : } (hp : ) (x : R) (y : R) (z : A) (h : β() p = 0) (hz : z * β() x = β() y) :
theorem Polynomial.Monic.leadingCoeff_not_mem {R : Type u} [] {π : } {f : } (hf : ) (h : π β  β€) :
theorem Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem {R : Type u} [] {π : } {f : } (hf : ) (h : π β  β€) (hmem : β {n : β}, β β π) (hnot_mem : Β¬ β π ^ 2) :
theorem Polynomial.IsEisensteinAt.isWeaklyEisensteinAt {R : Type u} [] {π : } {f : } (hf : ) :
theorem Polynomial.IsEisensteinAt.coeff_mem {R : Type u} [] {π : } {f : } (hf : ) {n : β} (hn : ) :
β π
theorem Polynomial.IsEisensteinAt.irreducible {R : Type u} [] [] {π : } {f : } (hf : ) (hprime : Ideal.IsPrime π) (hu : ) (hfd0 : ) :

If a primitive f satisfies f.IsEisensteinAt π, where π.IsPrime, then f is irreducible.