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 #

Main results #

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

structure Polynomial.IsWeaklyEisensteinAt {R : Type u} [CommSemiring R] (f : Polynomial R) (π“Ÿ : Ideal R) :

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
    structure Polynomial.IsEisensteinAt {R : Type u} [CommSemiring R] (f : Polynomial R) (π“Ÿ : Ideal R) :

    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} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : Polynomial.IsWeaklyEisensteinAt f π“Ÿ) {A : Type v} [CommRing A] (Ο† : R β†’+* A) :
      theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree_le {R : Type u} [CommRing R] {f : Polynomial R} {S : Type v} [CommRing S] [Algebra R S] {p : R} {x : S} (hx : ↑(Polynomial.aeval x) f = 0) (hmo : Polynomial.Monic f) (hf : Polynomial.IsWeaklyEisensteinAt f (Submodule.span R {p})) (i : β„•) :
      Polynomial.natDegree (Polynomial.map (algebraMap R S) f) ≀ i β†’ βˆƒ y, y ∈ Algebra.adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
      theorem Polynomial.dvd_pow_natDegree_of_evalβ‚‚_eq_zero {R : Type u} {A : Type u_1} [CommRing R] [CommRing A] {f : R β†’+* A} (hf : Function.Injective ↑f) {p : Polynomial R} (hp : Polynomial.Monic p) (x : R) (y : R) (z : A) (h : Polynomial.evalβ‚‚ f z p = 0) (hz : ↑f x * z = ↑f y) :
      theorem Polynomial.dvd_pow_natDegree_of_aeval_eq_zero {R : Type u} {A : Type u_1} [CommRing R] [CommRing A] [Algebra R A] [Nontrivial A] [NoZeroSMulDivisors R A] {p : Polynomial R} (hp : Polynomial.Monic p) (x : R) (y : R) (z : A) (h : ↑(Polynomial.aeval z) p = 0) (hz : z * ↑(algebraMap R A) x = ↑(algebraMap R A) y) :
      theorem Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem {R : Type u} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : Polynomial.Monic f) (h : π“Ÿ β‰  ⊀) (hmem : βˆ€ {n : β„•}, n < Polynomial.natDegree f β†’ Polynomial.coeff f n ∈ π“Ÿ) (hnot_mem : Β¬Polynomial.coeff f 0 ∈ π“Ÿ ^ 2) :
      theorem Polynomial.IsEisensteinAt.coeff_mem {R : Type u} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : Polynomial.IsEisensteinAt f π“Ÿ) {n : β„•} (hn : n β‰  Polynomial.natDegree f) :
      theorem Polynomial.IsEisensteinAt.irreducible {R : Type u} [CommRing R] [IsDomain R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : Polynomial.IsEisensteinAt f π“Ÿ) (hprime : Ideal.IsPrime π“Ÿ) (hu : Polynomial.IsPrimitive f) (hfd0 : 0 < Polynomial.natDegree f) :

      If a primitive f satisfies f.IsEisensteinAt π“Ÿ, where π“Ÿ.IsPrime, then f is irreducible.