leadingCoeff_mul_of_isRegular_right

English

Let f,g be mv polynomials over a commutative semiring with a fixed monomial order m. If f ≠ 0 and the leading coefficient of g is regular, then lc_m(fg) = lc_m(f) lc_m(g).

Русский

Пусть f и g — mv-многочлены над коммутативной полугруппой, упорядочение мономов m. Если f ≠ 0 и lc_m(g) регулярен, то lc_m(fg) = lc_m(f) lc_m(g).

LaTeX

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

Lean4

/-- Multiplicativity of leading coefficients -/
theorem leadingCoeff_mul_of_isRegular_right {f g : MvPolynomial σ R} (hf : f ≠ 0) (hg : IsRegular (m.leadingCoeff g)) :
    m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g := by
  simp only [leadingCoeff, degree_mul_of_isRegular_right hf hg, coeff_mul_of_degree_add]

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