degree_mul_of_mul_leadingCoeff_ne_zero

English

If deg g ≺ deg f, then deg(f+g) = deg f.

Русский

Если deg g меньше deg f, тогда deg(f+g) = deg f.

LaTeX

$$$m.degree g \prec_m m.degree f \Rightarrow m.degree (f+g) = m.degree f$$$

Lean4

/-- Monomial degree of product -/
theorem degree_mul_of_mul_leadingCoeff_ne_zero {f g : MvPolynomial σ R}
    (hfg : m.leadingCoeff f * m.leadingCoeff g ≠ 0) : m.degree (f * g) = m.degree f + m.degree g :=
  by
  apply m.toSyn.injective
  apply le_antisymm degree_mul_le
  apply le_degree
  rw [mem_support_iff, coeff_mul_of_degree_add]
  exact hfg

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