degree_mul_of_isRegular_left — Mathlib

English

If the leading coefficient of f is regular and g ≠ 0, then deg(fg) = deg f + deg g.

Русский

Если ведущий коэффициент f регулярный и g ≠ 0, тогда deg(fg) = deg f + deg g.

LaTeX

$$$m.leadingCoeff f \text{ is regular} \Rightarrow m.degree (f\*g) = m.degree f + m.degree g$$$

Lean4

/-- Monomial degree of product -/
theorem degree_mul_of_isRegular_left {f g : MvPolynomial σ R} (hf : IsRegular (m.leadingCoeff f)) (hg : g ≠ 0) :
    m.degree (f * g) = m.degree f + m.degree g :=
  by
  apply degree_mul_of_mul_leadingCoeff_ne_zero
  simp only [ne_eq, hf, IsRegular.left, IsLeftRegular.mul_left_eq_zero_iff, leadingCoeff_eq_zero_iff]
  exact hg

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