English
If φ lies in the weighted homogeneous submodule of degree n, then the m-th component equals p if m = n and 0 otherwise.
Русский
Если φ принадлежит подмодулю взвешенной однородности степени n, то компонентa m равна p при m = n и ноль иначе.
LaTeX
$$$p ∈ weightedHomogeneousSubmodule\, R\, w\, n \Rightarrow weightedHomogeneousComponent\, w\, m\, p = \begin{cases} p, & m = n \\ 0, & m ≠ n \end{cases}$$$
Lean4
/-- The weighted homogeneous components of a weighted homogeneous polynomial. -/
theorem weightedHomogeneousComponent_of_mem [DecidableEq M] {m n : M} {p : MvPolynomial σ R}
(h : p ∈ weightedHomogeneousSubmodule R w n) : weightedHomogeneousComponent w m p = if m = n then p else 0 :=
by
simp only [mem_weightedHomogeneousSubmodule] at h
ext x
rw [coeff_weightedHomogeneousComponent]
by_cases zero_coeff : coeff x p = 0
· split_ifs <;> simp only [zero_coeff, coeff_zero]
· rw [h zero_coeff]
simp only [show n = m ↔ m = n from eq_comm]
split_ifs with h1
· rfl
· simp only [coeff_zero]
