decompose'_apply — Mathlib

English

For any φ and weight w, the m-th component of the weighted decomposition of φ equals the weight-m homogeneous component of φ.

Русский

Для любого φ и веса w m-я компонента взвешенного разложения φ равна весовой компоненте φ с весом m.

LaTeX

$$$((\\text{weightedDecomposition } R w).decompose' \\phi)(m) = \\operatorname{weightedHomogeneousComponent} w m \\phi,$$$

Lean4

theorem decompose'_apply [DecidableEq M] (φ : MvPolynomial σ R) (m : M) :
    ((weightedDecomposition R w).decompose' φ m : MvPolynomial σ R) = weightedHomogeneousComponent w m φ :=
  MvPolynomial.decompose'_apply R w φ m

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