Theorems · Theorem · commutative algebra

Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map

∀ {R : Type u_1} [inst : 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 ⋯)

Defined in

Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished

Cited by

2 results in Mathlib

Foundations

Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing