decompose'_apply — Mathlib

English

For any φ and m, the m-th component of decompose'(R,w)φ equals the weighted homogeneous component with index m.

Русский

Для любого φ и m, m-ая компонента из decompose'(R,w)φ равна взвешенно однородной компоненте с индексом m.

LaTeX

$$$(\\mathrm{decompose}'(R,w)\\varphi)(m) = \\operatorname{weightedHomogeneousComponent}(w,m,\\varphi)$$$

Lean4

theorem decompose'_apply [DecidableEq M] (φ : MvPolynomial σ R) (m : M) :
    (decompose' R w φ m : MvPolynomial σ R) = weightedHomogeneousComponent w m φ :=
  by
  rw [decompose']
  by_cases hm : m ∈ Finset.image (weight w) φ.support
  · simp only [DirectSum.mk_apply_of_mem hm, Subtype.coe_mk]
  · rw [DirectSum.mk_apply_of_notMem hm, Submodule.coe_zero, weightedHomogeneousComponent_eq_zero_of_notMem w φ m hm]

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