homogeneousComponent — Mathlib

English

For each p, the p-th homogeneous component is a linear projection extracting exactly the p-th homogeneous part of a multivariate power series.

Русский

Для каждого p-я однородная компонента — это линейное отображение, извлекающее ровно p‑ю однородную часть ряда MvPowerSeries σ R.

LaTeX

$$homogeneousComponent(p) = weightedHomogeneousComponent(1, p)$$

Lean4

/-- The homogeneous components of an `MvPowerSeries` -/
def homogeneousComponent (p : ℕ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R :=
  weightedHomogeneousComponent 1 p

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