coeff_homogeneousComponent — Mathlib

English

For d a monomial exponent vector, the coefficient of d in the degree-n component is coeff_d( homogeneousComponent(n) φ ) = coeff_d(φ) if deg(d) = n, else 0.

Русский

Для каждого многочлена коэффициент монома с весом d в компоненте степени n равен coeff_d(φ) если deg(d)=n, иначе 0.

LaTeX

$$$\\forall d:\\sigma\\to\\mathbb{N},\\; coeff\\_d(homogeneousComponent(n)\\;φ) = \\begin{cases} coeff\\_d(φ), & d.degree = n \\\\ 0, & \\text{иначе} \\end{cases}$$$

Lean4

theorem coeff_homogeneousComponent (d : σ →₀ ℕ) :
    coeff d (homogeneousComponent n φ) = if d.degree = n then coeff d φ else 0 :=
  by
  rw [degree_eq_weight_one]
  convert coeff_weightedHomogeneousComponent n φ d

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