Documentation

Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Distinguished polynomial #

In this file we define the predicate Polynomial.IsDistinguishedAt and develop the most basic lemmas about it.

structure Polynomial.IsDistinguishedAt {R : Type u_1} [CommRing R] (f : Polynomial R) (I : Ideal R) extends f.IsWeaklyEisensteinAt I :

Given an ideal I of a commutative ring R, we say that a polynomial f : R[X] is Distinguished at I if f is monic and IsWeaklyEisensteinAt I. i.e. f is of the form xⁿ + a₁xⁿ⁻¹ + ⋯ + aₙ with aᵢ ∈ I for all i.

Instances For
    @[deprecated Polynomial.IsDistinguishedAt.map_eq_X_pow (since := "2025-04-27")]

    Alias of Polynomial.IsDistinguishedAt.map_eq_X_pow.

    theorem Polynomial.IsDistinguishedAt.degree_eq_order_map {R : Type u_1} [CommRing R] {I : Ideal R} (f h : PowerSeries R) {g : Polynomial R} (distinguish : g.IsDistinguishedAt I) (nmem : (PowerSeries.constantCoeff R) hI) (eq : f = g * h) :
    @[deprecated Polynomial.IsDistinguishedAt.degree_eq_order_map (since := "2025-04-27")]
    theorem IsDistinguishedAt.degree_eq_order_map {R : Type u_1} [CommRing R] {I : Ideal R} (f h : PowerSeries R) {g : Polynomial R} (distinguish : g.IsDistinguishedAt I) (nmem : (PowerSeries.constantCoeff R) hI) (eq : f = g * h) :

    Alias of Polynomial.IsDistinguishedAt.degree_eq_order_map.