coe_natDegree_eq_order_map — Mathlib

English

The natDegree of a distinguished polynomial equals the order of its map under the quotient, up to Cast into ENat.

Русский

Натуральная степень полинома с DistinguishedAt соответствует порядку отображения через тождественный отображатель модуля.

LaTeX

$$$f IsDistinguishedAt I \\to natDegree(f) = (f.map(\\mathrm{Quotient.mk} I)).order$$$

Lean4

theorem coe_natDegree_eq_order_map (distinguish : g.IsDistinguishedAt I) (notMem : PowerSeries.constantCoeff h ∉ I)
    (eq : f = g * h) : g.natDegree = (f.map (Ideal.Quotient.mk I)).order :=
  by
  rw [natDegree, distinguish.degree_eq_coe_lift_order_map f h notMem eq]
  exact ENat.coe_lift _ <| order_finite_iff_ne_zero.2 <| distinguish.map_ne_zero_of_eq_mul f h notMem eq

Похожие утверждения