weightedTotalDegree'_eq_bot_iff — Mathlib

English

For any weight w and polynomial p, the weightedTotalDegree' of p equals bottom if and only if p is the zero polynomial.

Русский

Для веса w и полинома p величина weightedTotalDegree'(p) равна ⊥ тогда и только тогда, когда p = 0.

LaTeX

$$$\weightedTotalDegree' w p = \bot \iff p = 0$$$

Lean4

/-- The `weightedTotalDegree'` of a polynomial `p` is `⊥` if and only if `p = 0`. -/
theorem weightedTotalDegree'_eq_bot_iff (w : σ → M) (p : MvPolynomial σ R) : weightedTotalDegree' w p = ⊥ ↔ p = 0 :=
  by
  simp only [weightedTotalDegree', Finset.sup_eq_bot_iff, mem_support_iff, WithBot.coe_ne_bot, MvPolynomial.eq_zero_iff]
  exact forall_congr' fun _ => Classical.not_not

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