English
If i is not in the image of weight w on φ.support, then the i-th weighted homogeneous component is zero.
Русский
Если i не принадлежит образу weight w на поддержке φ, то i-я взвешенная однородная компонента нулевая.
LaTeX
$$$i \notin \operatorname{image}(weight\, w)\; \varphi.support \Rightarrow weightedHomogeneousComponent\, w\, i\, \varphi = 0$$$
Lean4
/-- If `w` is a nontorsion weight function, then a multivariate polynomial has weighted total
degree zero if and only if for every `m ∈ p.support` and `x : σ`, `m x = 0`. -/
theorem weightedTotalDegree_eq_zero_iff (hw : NonTorsionWeight w) (p : MvPolynomial σ R) :
p.weightedTotalDegree w = 0 ↔ ∀ (m : σ →₀ ℕ) (_ : m ∈ p.support) (x : σ), m x = 0 :=
by
rw [← isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero, IsWeightedHomogeneous]
apply forall_congr'
intro m
rw [mem_support_iff]
apply forall_congr'
intro _
exact weightedDegree_eq_zero_iff hw
