weightedTotalDegree'_zero — Mathlib

English

The weightedTotalDegree' of the zero polynomial is the bottom element ⊥.

Русский

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

LaTeX

$$$\operatorname{weightedTotalDegree}' w (0 : \mathrm{MvPolynomial} \; \sigma\; R) = \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]

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