weightedTotalDegree_zero — Mathlib

English

The weighted total degree of the zero polynomial is the bottom element ⊥ of M.

Русский

Весовая суммарная степень нулевого многочлена равна нижней границе ⊥ в M.

LaTeX

$$$\\operatorname{weightedTotalDegree}(w,0)=\\bot$$$

Lean4

/-- The `weightedTotalDegree` of the zero polynomial is `⊥`. -/
theorem weightedTotalDegree_zero (w : σ → M) : weightedTotalDegree w (0 : MvPolynomial σ R) = ⊥ := by
  simp only [weightedTotalDegree, support_zero, Finset.sup_empty]

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