coeff_weightedHomogeneousComponent

English

For any d, the coefficient of d in the projected weighted homogeneous component equals coeff d φ if the weight matches the target n, otherwise it is 0.

Русский

Для любого d коэффициент d в компоненте взвешенно однородного проекции равен coeff d φ, если weight w d = n, иначе 0.

LaTeX

$$coeff d (weightedHomogeneousComponent w n φ) = if weight w d = n then coeff d φ else 0$$

Lean4

theorem coeff_weightedHomogeneousComponent [DecidableEq M] (d : σ →₀ ℕ) :
    coeff d (weightedHomogeneousComponent w n φ) = if weight w d = n then coeff d φ else 0 :=
  letI := Classical.decEq M
  Finsupp.filter_apply (fun d : σ →₀ ℕ => weight w d = n) φ d |>.trans <| by convert rfl

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