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 : Prop

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.

• mem {n : ℕ} : n < f.natDegree → f.coeff n ∈ I
• monic : f.Monic

theorem Polynomial.IsDistinguishedAt.map_eq_X_pow {R : Type u_1} [CommRing R] {f : Polynomial R} {I : Ideal R} (distinguish : f.IsDistinguishedAt I) : map (Ideal.Quotient.mk I) f = X ^ f.natDegree

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

theorem IsDistinguishedAt.map_eq_X_pow {R : Type u_1} [CommRing R] {f : Polynomial R} {I : Ideal R} (distinguish : f.IsDistinguishedAt I) : Polynomial.map (Ideal.Quotient.mk I) f = Polynomial.X ^ f.natDegree

Alias of Polynomial.IsDistinguishedAt.map_eq_X_pow.

theorem Polynomial.IsDistinguishedAt.map_ne_zero_of_eq_mul {R : Type u_1} [CommRing R] {I : Ideal R} (f h : PowerSeries R) {g : Polynomial R} (distinguish : g.IsDistinguishedAt I) (nmem : (PowerSeries.constantCoeff R) h ∉ I) (eq : f = ↑g * h) : (PowerSeries.map (Ideal.Quotient.mk I)) f ≠ 0

theorem Polynomial.IsDistinguishedAt.degree_eq_coe_lift_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) h ∉ I) (eq : f = ↑g * h) : g.degree = ↑(((PowerSeries.map (Ideal.Quotient.mk I)) f).order.lift ⋯)

@[deprecated Polynomial.IsDistinguishedAt.degree_eq_coe_lift_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) h ∉ I) (eq : f = ↑g * h) : g.degree = ↑(((PowerSeries.map (Ideal.Quotient.mk I)) f).order.lift ⋯)

Alias of Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map.

@[deprecated Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map (since := "2025-05-19")]

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) h ∉ I) (eq : f = ↑g * h) : g.degree = ↑(((PowerSeries.map (Ideal.Quotient.mk I)) f).order.lift ⋯)

Alias of Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map.

theorem Polynomial.IsDistinguishedAt.coe_natDegree_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) h ∉ I) (eq : f = ↑g * h) : ↑g.natDegree = ((PowerSeries.map (Ideal.Quotient.mk I)) f).order