natDegree_eq_toNat_order_map — Mathlib

English

For a Weierstrass factorization g = f h, the natural degree of f equals the natural image of the order of g in the residue field.

Русский

Для факторизации g = f h натуральная степень f равна натуральному образу порядка g в поле остатков.

LaTeX

$$$\deg_{\text{nat}}(f) = (\operatorname{ord}((g \bmod \mathfrak{m})).to\,Nat)$$$

Lean4

theorem natDegree_eq_toNat_order_map : f.natDegree = (g.map (IsLocalRing.residue A)).order.toNat :=
  H.natDegree_eq_toNat_order_map_of_ne_top (Ideal.IsMaximal.ne_top inferInstance)

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