mvPolynomialBasis_repr_D_X — Mathlib

English

The image of the derivation D on the variable X_i under the mvPolynomialBasis repr is the basis element with coefficient 1 at i.

Русский

Изображение D на X_i через отображение repr даёт базисный элемент с коэффициентом 1 в позиции i.

LaTeX

$$$(mvPolynomialBasis\\; R\\; \\sigma).repr\\, (D\\; R\\; (MvPolynomial\\; \\sigma\\; R))\\, (X_i) = \\mathsf{Finsupp}.single(i,1).$$$

Lean4

@[simp]
theorem mvPolynomialBasis_repr_D_X (σ) (i) : (mvPolynomialBasis R σ).repr (D _ _ (.X i)) = Finsupp.single i 1 := by
  simp [mvPolynomialBasis_repr_D]

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