degree_eq_coe_lift_order_map_of_ne_top

English

If I ≠ ⊤ and g IsWeierstrassFactorizationAt f h I, then f.natDegree equals the lifted order of g modulo I.

Русский

Пусть I ≠ ⊤ и g IsWeierstrassFactorizationAt f h I; тогда natDegree f равен поднесённому порядку образа g по I.

LaTeX

$$f.natDegree = (g.map (Ideal.Quotient.mk I)).order.lift (order_finite_iff_ne_zero.2 (H.map_ne_zero_of_ne_top hI))$$

Lean4

theorem degree_eq_coe_lift_order_map_of_ne_top (hI : I ≠ ⊤) :
    f.degree = (g.map (Ideal.Quotient.mk I)).order.lift (order_finite_iff_ne_zero.2 (H.map_ne_zero_of_ne_top hI)) :=
  by
  refine H.isDistinguishedAt.degree_eq_coe_lift_order_map g h ?_ H.eq_mul
  contrapose! hI
  exact Ideal.eq_top_of_isUnit_mem _ hI (isUnit_iff_constantCoeff.1 H.isUnit)

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