totalDegree_eq_zero_iff — Mathlib

English

A polynomial has total degree zero iff every monomial in its support has all variables having exponent zero (i.e., the polynomial is constant).

Русский

Полином имеет общую степень ноль тогда и только тогда, когда каждая мономика в его опорe имеет нулевые степени переменных (полином константен).

LaTeX

$$$p.totalDegree = 0 \\iff \\forall m \\in p.support, \\forall x, m(x) = 0$$$

Lean4

theorem totalDegree_eq_zero_iff (p : MvPolynomial σ R) :
    p.totalDegree = 0 ↔ ∀ (m : σ →₀ ℕ) (_ : m ∈ p.support) (x : σ), m x = 0 :=
  by
  rw [← weightedTotalDegree_one, weightedTotalDegree_eq_zero_iff _ p]
  exact nonTorsionWeight_of (Function.const σ one_ne_zero)

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