weightedHomogeneousComponent_mem — Mathlib

English

The weighted homogeneous component of degree m of φ lies in the corresponding weighted homogeneous submodule.

Русский

Взвешенная однородная компонента степени m полинома φ принадлежит соответствующему взвешенно однородному подмодулю.

LaTeX

$$$weightedHomogeneousComponent\, w\, m\, \varphi \in weightedHomogeneousSubmodule\, R\, w\, m$$$

Lean4

theorem weightedHomogeneousComponent_mem (w : σ → M) (φ : MvPolynomial σ R) (m : M) :
    weightedHomogeneousComponent w m φ ∈ weightedHomogeneousSubmodule R w m :=
  by
  rw [mem_weightedHomogeneousSubmodule]
  exact weightedHomogeneousComponent_isWeightedHomogeneous m φ

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