English
The weighted homogeneous component of weight p of f is the power series whose coefficient at d is coeff d f if weight w d = p, and 0 otherwise.
Русский
Весовой компонент веса p для f имеет коэффициент при d равный coeff d f, если weight w d = p, и 0 в противном случае.
LaTeX
$$$ (\mathrm{weightedHomogeneousComponent}\ w\ p\ f)_d = \begin{cases} \operatorname{coeff}_d f, & w(d) = p, \\ 0, & \text{иначе}. \end{cases} $$$
Lean4
/-- The weighted homogeneous components of an `MvPowerSeries f`. -/
def weightedHomogeneousComponent (p : ℕ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R
where
toFun f d := if weight w d = p then coeff d f else 0
map_add' f
g := by
ext d
simp only [map_add, coeff_apply]
split_ifs with h
· rfl
· rw [add_zero]
map_smul' a
f := by
ext d
simp only [map_smul, smul_eq_mul, RingHom.id_apply, coeff_apply, mul_ite, mul_zero]
