mvPolynomialBasis_repr_apply — Mathlib

English

For each i, the coefficient of i in the representation of D applied to a polynomial is the pderiv with respect to i.

Русский

Для каждого i коэффициент представления D по переменной i равен pderiv по i.

LaTeX

$$$\\text{repr}(D\\; x)\\; i = \\mathrm{pderiv}\\_i(x).$$$

Lean4

@[simp]
theorem mvPolynomialBasis_repr_apply (σ) (x) (i) : (mvPolynomialBasis R σ).repr (D _ _ x) i = MvPolynomial.pderiv i x :=
  by
  classical
  suffices ((Finsupp.lapply i).comp (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
    rw [← this]; rfl
  apply MvPolynomial.derivation_ext
  intro j
  simp [Finsupp.single_apply, Pi.single_apply]

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