homogeneousComponent_apply — Mathlib

English

The homogeneous component is given by summing monomials with degree equal to n and coefficients preserved; i.e., homogeneousComponent(n) φ equals the sum over d ∈ supp(φ) with deg(d)=n of monomial d (coeff d φ).

Русский

Компонента по степени n равна сумме мономиов степени n с сохранением коэффициентов: homogeneousComponent(n) φ = ∑_{d ∈ supp(φ), deg(d)=n} monomial d (coeff d φ).

LaTeX

$$$homogeneousComponent(n)\\;φ = \\sum_{d ∈ φ.support, \\; d.degree = n} monomial(d, coeff\\_d(φ))$$$

Lean4

theorem homogeneousComponent_apply :
    homogeneousComponent n φ = ∑ d ∈ φ.support with d.degree = n, monomial d (coeff d φ) :=
  by
  simp_rw [degree_eq_weight_one]
  convert weightedHomogeneousComponent_apply n φ

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