mathlib documentation

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 #

Main results #

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).

source
theorem polynomial.is_weakly_eisenstein_at_iff {R : Type u} [comm_semiring R] (f : R[X]) (π“Ÿ : ideal R) :
f.is_weakly_eisenstein_at Β«π“ŸΒ» ↔ βˆ€ {n : β„•}, n < f.nat_degree β†’ f.coeff n ∈ Β«π“ŸΒ»
source
structure polynomial.is_weakly_eisenstein_at {R : Type u} [comm_semiring R] (f : R[X]) (π“Ÿ : 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 ∈ π“Ÿ.

source
structure polynomial.is_eisenstein_at {R : Type u} [comm_semiring R] (f : R[X]) (π“Ÿ : 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.

source
theorem polynomial.is_eisenstein_at_iff {R : Type u} [comm_semiring R] (f : R[X]) (π“Ÿ : ideal R) :
f.is_eisenstein_at Β«π“ŸΒ» ↔ f.leading_coeff βˆ‰ Β«π“ŸΒ» ∧ (βˆ€ {n : β„•}, n < f.nat_degree β†’ f.coeff n ∈ Β«π“ŸΒ») ∧ f.coeff 0 βˆ‰ Β«π“ŸΒ» ^ 2
source
theorem polynomial.is_weakly_eisenstein_at.map {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at Β«π“ŸΒ») {A : Type v} [comm_ring A] (Ο† : R β†’+* A) :
(polynomial.map Ο† f).is_weakly_eisenstein_at (ideal.map Ο† Β«π“ŸΒ»)
source
theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree {R : Type u} [comm_ring R] {f : R[X]} {S : Type v} [comm_ring S] [algebra R S] {p : R} {x : S} (hx : ⇑(polynomial.aeval x) f = 0) (hmo : f.monic) (hf : f.is_weakly_eisenstein_at (submodule.span R {p})) :
βˆƒ (y : S) (H : y ∈ algebra.adjoin R {x}), (⇑(algebra_map R S) p) * y = x ^ (polynomial.map (algebra_map R S) f).nat_degree
source
theorem polynomial.is_weakly_eisenstein_at.exists_mem_adjoin_mul_eq_pow_nat_degree_le {R : Type u} [comm_ring R] {f : R[X]} {S : Type v} [comm_ring S] [algebra R S] {p : R} {x : S} (hx : ⇑(polynomial.aeval x) f = 0) (hmo : f.monic) (hf : f.is_weakly_eisenstein_at (submodule.span R {p})) (i : β„•) :
(polynomial.map (algebra_map R S) f).nat_degree ≀ i β†’ (βˆƒ (y : S) (H : y ∈ algebra.adjoin R {x}), (⇑(algebra_map R S) p) * y = x ^ i)
source
theorem polynomial.is_weakly_eisenstein_at.pow_nat_degree_le_of_root_of_monic_mem {R : Type u} [comm_ring R] {π“Ÿ : ideal R} {f : R[X]} (hf : f.is_weakly_eisenstein_at Β«π“ŸΒ») {x : R} (hroot : f.is_root x) (hmo : f.monic) (i : β„•) :
f.nat_degree ≀ i β†’ x ^ i ∈ Β«π“ŸΒ»
source
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 : R[X]} (hf : f.is_weakly_eisenstein_at Β«π“ŸΒ») {S : Type v} [comm_ring S] [algebra R S] {x : S} (hx : ⇑(polynomial.aeval x) f = 0) (hmo : f.monic) (i : β„•) :
(polynomial.map (algebra_map R S) f).nat_degree ≀ i β†’ x ^ i ∈ ideal.map (algebra_map R S) Β«π“ŸΒ»
source
theorem polynomial.is_eisenstein_at.is_weakly_eisenstein_at {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : R[X]} (hf : f.is_eisenstein_at Β«π“ŸΒ») :
f.is_weakly_eisenstein_at Β«π“ŸΒ»
source
theorem polynomial.is_eisenstein_at.coeff_mem {R : Type u} [comm_semiring R] {π“Ÿ : ideal R} {f : R[X]} (hf : f.is_eisenstein_at Β«π“ŸΒ») {n : β„•} (hn : n β‰  f.nat_degree) :
f.coeff n ∈ Β«π“ŸΒ»
source
theorem polynomial.is_eisenstein_at.irreducible {R : Type u} [comm_ring R] [is_domain R] {π“Ÿ : ideal R} {f : R[X]} (hf : f.is_eisenstein_at Β«π“ŸΒ») (hprime : Β«π“ŸΒ».is_prime) (hu : f.is_primitive) (hfd0 : 0 < f.nat_degree) :
irreducible f

If a primitive f satisfies f.is_eisenstein_at π“Ÿ, where π“Ÿ.is_prime, then f is irreducible.