coeff_homogeneousComponent — Mathlib

English

For all p and all d, the coefficient of d in the p-th homogeneous component of f equals the coefficient of d in f if deg(d) = p, and is 0 otherwise.

Русский

Для всех p и d коэффициент d в p-й однородной компоненте f равен коэффициенту d в f, если deg(d) = p, иначе равен 0.

LaTeX

$$coeff_d(homogeneousComponent(p) f) = if degree(d) = p then coeff_d f else 0$$

Lean4

theorem coeff_homogeneousComponent (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R) :
    coeff d (homogeneousComponent p f) = if degree d = p then coeff d f else 0 :=
  by
  rw [degree_eq_weight_one]
  exact coeff_weightedHomogeneousComponent 1 p d f

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