totalDegree_mul_of_isDomain — Mathlib

English

Over a domain, for nonzero multivariate polynomials f and g, the total degree is additive under multiplication: totalDegree(fg) = totalDegree(f) + totalDegree(g).

Русский

В области произведение полинома и другого полинома суммарной степени даёт сумму степеней: totalDegree(fg) = totalDegree(f) + totalDegree(g).

LaTeX

$$$[IsCancelMulZero R] \\; f \\neq 0 \\; \\&\\; g \\neq 0 \\Rightarrow \\operatorname{totalDegree}(f g) = \\operatorname{totalDegree}(f) + \\operatorname{totalDegree}(g)$$$

Lean4

theorem totalDegree_mul_of_isDomain [IsCancelMulZero R] (hf : f ≠ 0) (hg : g ≠ 0) :
    totalDegree (f * g) = totalDegree f + totalDegree g :=
  by
  cases exists_wellOrder σ
  rw [← degree_degLexDegree (σ := σᵒᵈ), ← degree_degLexDegree (σ := σᵒᵈ), ← degree_degLexDegree (σ := σᵒᵈ),
    MonomialOrder.degree_mul hf hg]
  simp

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