# mathlib3documentation

ring_theory.polynomial.eisenstein.basic

# Eisenstein polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.

## 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) :
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) :
f.is_eisenstein_at π β f.leading_coeff β π β§ (β {n : β}, n < f.nat_degree β f.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) :
(ideal.map Ο π)
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 : β) :
β x ^ 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 : β) :
theorem polynomial.scale_roots.is_weakly_eisenstein_at {R : Type u} [comm_ring R] (p : polynomial R) {x : R} {P : ideal R} (hP : x β P) :
theorem polynomial.dvd_pow_nat_degree_of_evalβ_eq_zero {R : Type u} {A : Type u_1} [comm_ring R] [comm_ring A] {f : R β+* A} (hf : function.injective βf) {p : polynomial R} (hp : p.monic) (x y : R) (z : A) (h : p = 0) (hz : βf x * z = βf y) :
theorem polynomial.dvd_pow_nat_degree_of_aeval_eq_zero {R : Type u} {A : Type u_1} [comm_ring R] [comm_ring A] [ A] [nontrivial A] {p : polynomial R} (hp : p.monic) (x y : R) (z : A) (h : p = 0) (hz : z * β A) x = β A) y) :
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_degree β f.coeff n β π) (hnot_mem : f.coeff 0 β π ^ 2) :
f.is_eisenstein_at π
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.