degree_mul — Mathlib

English

Let f,g be mv polynomials with f ≠ 0 and lc_m(g) regular. Then deg_m(fg) = deg_m(f) + deg_m(g).

Русский

Пусть f и g — mv-многочлены, f ≠ 0 и lc_m(g) регулярен. Тогда deg_m(fg) = deg_m(f) + deg_m(g).

LaTeX

$$$$ \deg_m(fg) = \deg_m(f) + \deg_m(g), \quad \text{provided } f \neq 0 \text{ and } \operatorname{IsRegular}(\operatorname{leadingCoeff}_m(g)). $$$$

Lean4

/-- Monomial degree of product -/
theorem degree_mul [IsCancelMulZero R] {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : g ≠ 0) :
    m.degree (f * g) = m.degree f + m.degree g :=
  degree_mul_of_isRegular_left (isRegular_of_ne_zero (leadingCoeff_ne_zero_iff.mpr hf)) hg

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