English
For each w: σ → M and m ∈ M, the set {p : MvPolynomial σ R | p is weighted homogeneous of degree m} forms an R-submodule of MvPolynomial σ R.
Русский
Пусть w: σ → M и m ∈ M. Тогда множество всех многочленов, взвешенно однородных степени m, образует R-подмодуль в MvPolynomial σ R.
LaTeX
$$def weightedHomogeneousSubmodule (w : σ → M) (m : M) : Submodule R (MvPolynomial σ R)$$
Lean4
/-- The submodule of homogeneous `MvPolynomial`s of degree `n`. -/
def weightedHomogeneousSubmodule (w : σ → M) (m : M) : Submodule R (MvPolynomial σ R)
where
carrier := {x | x.IsWeightedHomogeneous w m}
smul_mem' r a ha c
hc := by
rw [coeff_smul] at hc
exact ha (right_ne_zero_of_mul hc)
zero_mem' _ hd := False.elim (hd <| coeff_zero _)
add_mem' {a} {b} ha hb c
hc := by
rw [coeff_add] at hc
obtain h | h : coeff c a ≠ 0 ∨ coeff c b ≠ 0 := by
contrapose! hc
simp only [hc, add_zero]
· exact ha h
· exact hb h
