English
Let f and g be multivariate polynomials over a commutative semiring with a fixed monomial order m. If the leading coefficient of f is regular with respect to m and g is nonzero, then the leading coefficient of the product f g equals the product of the leading coefficients: lc_m(fg) = lc_m(f) lc_m(g).
Русский
Пусть f и g — многочлены в нескольких переменных над коммутативной полугруппой, задан упорядочением мономов m. Если ведущий коэффициент f относительно m является регулярным, и g ≠ 0, то ведущий коэффициент произведения равен произведению ведущих коэффициентов: 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 } \operatorname{IsRegular}(\operatorname{leadingCoeff}_m(f)) \text{ and } g \neq 0. $$$$
Lean4
/-- Multiplicativity of leading coefficients -/
theorem leadingCoeff_mul_of_isRegular_left {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g ≠ 0) :
m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g := by
simp only [leadingCoeff, degree_mul_of_isRegular_left hf hg, coeff_mul_of_degree_add]
