homogeneousComponent_mem — Mathlib

English

For any n, and any φ ∈ MvPolynomial(σ, R), the homogeneous component of degree n, homogeneousComponent(n) φ, lies in the homogeneousSubmodule σ R n.

Русский

Для любого n и любого φ из MvPolynomial(σ, R) компонент степени n, homogeneousComponent(n) φ, принадлежит подмодулю homogeneousSubmodule σ R n.

LaTeX

$$$homogeneousComponent\\ n\\;φ \\in homogeneousSubmodule\\ σ\\ R\\ n$$$

Lean4

theorem homogeneousComponent_mem : homogeneousComponent n φ ∈ homogeneousSubmodule σ R n :=
  weightedHomogeneousComponent_mem _ φ n

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