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

theorem Polynomial.isWeaklyEisensteinAt_iff {R : Type u} [CommSemiring R] (f : Polynomial R) (π“Ÿ : Ideal R) :
f.IsWeaklyEisensteinAt π“Ÿ ↔ βˆ€ {n : β„•}, n < f.natDegree β†’ f.coeff n ∈ π“Ÿ
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 ∈ π“Ÿ.

  • mem : βˆ€ {n : β„•}, n < f.natDegree β†’ f.coeff n ∈ π“Ÿ
Instances For
    theorem Polynomial.IsWeaklyEisensteinAt.mem {R : Type u} [CommSemiring R] {f : Polynomial R} {π“Ÿ : Ideal R} (self : f.IsWeaklyEisensteinAt π“Ÿ) {n : β„•} :
    n < f.natDegree β†’ f.coeff n ∈ π“Ÿ
    theorem Polynomial.isEisensteinAt_iff {R : Type u} [CommSemiring R] (f : Polynomial R) (π“Ÿ : Ideal R) :
    f.IsEisensteinAt π“Ÿ ↔ f.leadingCoeff βˆ‰ π“Ÿ ∧ (βˆ€ {n : β„•}, n < f.natDegree β†’ f.coeff n ∈ π“Ÿ) ∧ f.coeff 0 βˆ‰ π“Ÿ ^ 2
    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.

    • leading : f.leadingCoeff βˆ‰ π“Ÿ
    • mem : βˆ€ {n : β„•}, n < f.natDegree β†’ f.coeff n ∈ π“Ÿ
    • not_mem : f.coeff 0 βˆ‰ π“Ÿ ^ 2
    Instances For
      theorem Polynomial.IsEisensteinAt.leading {R : Type u} [CommSemiring R] {f : Polynomial R} {π“Ÿ : Ideal R} (self : f.IsEisensteinAt π“Ÿ) :
      f.leadingCoeff βˆ‰ π“Ÿ
      theorem Polynomial.IsEisensteinAt.mem {R : Type u} [CommSemiring R] {f : Polynomial R} {π“Ÿ : Ideal R} (self : f.IsEisensteinAt π“Ÿ) {n : β„•} :
      n < f.natDegree β†’ f.coeff n ∈ π“Ÿ
      theorem Polynomial.IsEisensteinAt.not_mem {R : Type u} [CommSemiring R] {f : Polynomial R} {π“Ÿ : Ideal R} (self : f.IsEisensteinAt π“Ÿ) :
      f.coeff 0 βˆ‰ π“Ÿ ^ 2
      theorem Polynomial.IsWeaklyEisensteinAt.map {R : Type u} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.IsWeaklyEisensteinAt π“Ÿ) {A : Type v} [CommRing A] (Ο† : R β†’+* A) :
      (Polynomial.map Ο† f).IsWeaklyEisensteinAt (Ideal.map Ο† π“Ÿ)
      theorem Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree {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 : f.Monic) (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) :
      βˆƒ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
      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 : f.Monic) (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) (i : β„•) :
      (Polynomial.map (algebraMap R S) f).natDegree ≀ i β†’ βˆƒ y ∈ Algebra.adjoin R {x}, (algebraMap R S) p * y = x ^ i
      theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem {R : Type u} [CommRing R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.IsWeaklyEisensteinAt π“Ÿ) {x : R} (hroot : f.IsRoot x) (hmo : f.Monic) (i : β„•) :
      f.natDegree ≀ i β†’ x ^ i ∈ π“Ÿ
      theorem Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map {R : Type u} [CommRing R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.IsWeaklyEisensteinAt π“Ÿ) {S : Type v} [CommRing S] [Algebra R S] {x : S} (hx : (Polynomial.aeval x) f = 0) (hmo : f.Monic) (i : β„•) :
      (Polynomial.map (algebraMap R S) f).natDegree ≀ i β†’ x ^ i ∈ Ideal.map (algebraMap R S) π“Ÿ
      theorem Polynomial.scaleRoots.isWeaklyEisensteinAt {R : Type u} [CommRing R] (p : Polynomial R) {x : R} {P : Ideal R} (hP : x ∈ P) :
      (p.scaleRoots x).IsWeaklyEisensteinAt P
      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 : p.Monic) (x : R) (y : R) (z : A) (h : Polynomial.evalβ‚‚ f z p = 0) (hz : f x * z = f y) :
      x ∣ y ^ p.natDegree
      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 : p.Monic) (x : R) (y : R) (z : A) (h : (Polynomial.aeval z) p = 0) (hz : z * (algebraMap R A) x = (algebraMap R A) y) :
      x ∣ y ^ p.natDegree
      theorem Polynomial.Monic.leadingCoeff_not_mem {R : Type u} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.Monic) (h : π“Ÿ β‰  ⊀) :
      f.leadingCoeff βˆ‰ π“Ÿ
      theorem Polynomial.Monic.isEisensteinAt_of_mem_of_not_mem {R : Type u} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.Monic) (h : π“Ÿ β‰  ⊀) (hmem : βˆ€ {n : β„•}, n < f.natDegree β†’ f.coeff n ∈ π“Ÿ) (hnot_mem : f.coeff 0 βˆ‰ π“Ÿ ^ 2) :
      f.IsEisensteinAt π“Ÿ
      theorem Polynomial.IsEisensteinAt.isWeaklyEisensteinAt {R : Type u} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.IsEisensteinAt π“Ÿ) :
      f.IsWeaklyEisensteinAt π“Ÿ
      theorem Polynomial.IsEisensteinAt.coeff_mem {R : Type u} [CommSemiring R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.IsEisensteinAt π“Ÿ) {n : β„•} (hn : n β‰  f.natDegree) :
      f.coeff n ∈ π“Ÿ
      theorem Polynomial.IsEisensteinAt.irreducible {R : Type u} [CommRing R] [IsDomain R] {π“Ÿ : Ideal R} {f : Polynomial R} (hf : f.IsEisensteinAt π“Ÿ) (hprime : π“Ÿ.IsPrime) (hu : f.IsPrimitive) (hfd0 : 0 < f.natDegree) :

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