mul — Mathlib

English

If g is a Weierstrass factorization of f,h and g' is a Weierstrass factorization of f',h', then the product g g' is a Weierstrass factorization of f f', h h'.

Русский

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

LaTeX

$$g.IsWeierstrassFactorizationAt f h I → g'.IsWeierstrassFactorizationAt f' h' I → (g g').IsWeierstrassFactorizationAt (f f') (h h') I$$

Lean4

theorem mul {g' : A⟦X⟧} {f' : A[X]} {h' : A⟦X⟧} (H' : g'.IsWeierstrassFactorizationAt f' h' I) :
    (g * g').IsWeierstrassFactorizationAt (f * f') (h * h') I :=
  ⟨H.isDistinguishedAt.mul H'.isDistinguishedAt, H.isUnit.mul H'.isUnit, by
    rw [H.eq_mul, H'.eq_mul, Polynomial.coe_mul]; ring⟩

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