map_ne_zero_of_ne_top — Mathlib

English

If g is a Weierstrass factorization of f,h with respect to I, and g' is a Weierstrass factorization of f',h' with respect to I, then g g' is a Weierstrass factorization of f f', h h' with respect to I.

Русский

Если g является факторизацией Вайершстраса f,h по I, и g' — факторизацией f',h' по I, тогда произведение g g' является факторизацией f f', h h' по I.

LaTeX

$$(g IsWeierstrassFactorizationAt f h I) -> (g' IsWeierstrassFactorizationAt f' h' I) -> (g g').IsWeierstrassFactorizationAt (f f') (h h') I$$

Lean4

theorem map_ne_zero_of_ne_top (hI : I ≠ ⊤) : g.map (Ideal.Quotient.mk I) ≠ 0 :=
  by
  have := Ideal.Quotient.nontrivial hI
  rw [congr(map (Ideal.Quotient.mk I) $(H.eq_mul)), map_mul, ← Polynomial.polynomial_map_coe, ne_eq,
    (H.isUnit.map _).mul_left_eq_zero]
  exact_mod_cast f.map_monic_ne_zero (f := Ideal.Quotient.mk I) H.isDistinguishedAt.monic

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