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.mul {R : Type u_1} [CommRing R] {f f' : Polynomial R} {I : Ideal R} (hf : f.IsDistinguishedAt I) (hf' : f'.IsDistinguishedAt I) : (f * f').IsDistinguishedAt I

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

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

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