degree_mul_of_isRegular_right — Mathlib

English

Let f,g be multivariate polynomials over a commutative semiring with a fixed monomial order m. If f ≠ 0 and the leading coefficient of g is regular, then the degree with respect to m of the product equals the sum of degrees: deg_m(fg) = deg_m(f) + deg_m(g).

Русский

Пусть f, g — многочлены над полем/кольцом с упорядочением мономов m. Если 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_of_isRegular_right {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : IsRegular (m.leadingCoeff g)) :
    m.degree (f * g) = m.degree f + m.degree g := by rw [mul_comm, m.degree_mul_of_isRegular_left hg hf, add_comm]

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