English
If w is a non-torsion weight and p is a polynomial, then p is weighted homogeneous of degree 0 if and only if its weighted total degree is 0.
Русский
Если w — неторсионный вес и p — полином, то p взвешенно однороден нулевой степени тогда и только тогда, когда его взвешенная общая степень равна нулю.
LaTeX
$$$IsWeightedHomogeneous\, w\, p\, 0 \;\Leftrightarrow\; p.weightedTotalDegree\, w = 0$$$
Lean4
/-- If `w` is a nontorsion weight function, then the finitely supported function `m : σ →₀ ℕ`
has weighted degree zero if and only if `∀ x : σ, m x = 0`. -/
theorem weightedDegree_eq_zero_iff [CanonicallyOrderedAdd M] (hw : NonTorsionWeight w) {m : σ →₀ ℕ} :
weight w m = 0 ↔ ∀ x : σ, m x = 0 :=
by
simp only [weight, Finsupp.linearCombination, LinearMap.toAddMonoidHom_coe, coe_lsum, LinearMap.coe_smulRight,
LinearMap.id_coe, id_eq]
rw [Finsupp.sum, Finset.sum_eq_zero_iff]
apply forall_congr'
intro x
rw [Finsupp.mem_support_iff]
constructor
· intro hx
by_contra hx'
exact absurd (hw _ _ (hx hx')) hx'
· intro hax _
simp only [hax, zero_smul]
