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

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