weightedHomogeneousComponent_apply

English

For a weight function w: σ → M, the n-th weighted homogeneous component of a multivariate polynomial φ is the sum of monomials whose weight equals n with their coefficients.

Русский

Для весовой функции w: σ → M n-я взвешенно однородная компонента полинома φ является суммой мономов, чья весовая метка равна n, с их коэффициентами.

LaTeX

$$$\\operatorname{weightedHomogeneousComponent}(w,n)\\;\\varphi = \\sum_{d \\in \\operatorname{supp}(\\varphi), w(d)=n} \\mathrm{monomial}(d, \\varphi_d)$$$

Lean4

theorem weightedHomogeneousComponent_apply [DecidableEq M] :
    weightedHomogeneousComponent w n φ = ∑ d ∈ φ.support with weight w d = n, monomial d (coeff d φ) :=
  letI := Classical.decEq M
  Finsupp.filter_eq_sum (fun d : σ →₀ ℕ => weight w d = n) φ |>.trans <| by convert rfl

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