mvPolynomialBasis_repr_D — Mathlib

English

The representation of D applied to the polynomial ring generators via mvPolynomialBasis is exactly the derivation that maps X_i to the corresponding pderiv coefficient.

Русский

Представление D, применённого к базису mvPolynomialBasis, совпадает с выводом производной по соответствующему индексу.

LaTeX

$$$(mvPolynomialBasis\\; R\\; \\sigma).repr\\, (D\\; R\\; (MvPolynomial\\; \\sigma\\; R)) = \\text{coefficients given by } pderiv.$$$

Lean4

theorem mvPolynomialBasis_repr_D (σ) (x) :
    (mvPolynomialBasis R σ).repr (D _ _ x) = MvPolynomial.mkDerivation R (Finsupp.single · (1 : MvPolynomial σ R)) x :=
  Derivation.congr_fun (mvPolynomialBasis_repr_comp_D R σ) x

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