# 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 : ) (𝓟 : ) :
• mem : ∀ {n : }, 𝓟

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 : ) (𝓟 : ) :
• mem : ∀ {n : }, 𝓟
• not_mem : ¬ 𝓟 ^ 2

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) iy, 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) :
x
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) :
x
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 : ) (hu : ) (hfd0 : ) :

If a primitive f satisfies f.IsEisensteinAt 𝓟, where 𝓟.IsPrime, then f is irreducible.