English
For any commutative semiring R, and any n, the map homogeneousComponent(n) gives the degree-n part of a polynomial φ ∈ MvPolynomial(σ, R); this is a linear projection.
Русский
Для любой кольцевой системы R и любого n отображение homogeneousComponent(n) выделяет часть многочлена φ, однородную по степени n; это линейный проекционный оператор.
LaTeX
$$$\\text{homogeneousComponent}:\\;\\mathbb{N} \\to (MvPolynomial(σ,R) \\to\\_l[R] MvPolynomial(σ,R))$ и для всех $φ$, $homogeneousComponent(n)\\,φ$ является проекцией на однородную часть степени $n$.$$
Lean4
/-- `homogeneousComponent n φ` is the part of `φ` that is homogeneous of degree `n`.
See `sum_homogeneousComponent` for the statement that `φ` is equal to the sum
of all its homogeneous components. -/
def homogeneousComponent [CommSemiring R] (n : ℕ) : MvPolynomial σ R →ₗ[R] MvPolynomial σ R :=
weightedHomogeneousComponent 1 n
