mvPolynomialBasis_repr_symm_single

English

The inverse of the mvPolynomialBasis repr sends a basis element corresponding to i with coefficient x to x times D_R(MvPolynomial)(X_i).

Русский

Обратное отображение mvPolynomialBasis repr отправляет элемент базиса, соответствующий i, в x·D(X_i).

LaTeX

$$$\\text{(mvPolynomialBasis R σ).repr.symm}(\\mathsf{single}(i,x)) = x \\cdot D\\;R\\; (MvPolynomial\\; σ\\; R)\\; (X_i).$$$

Lean4

theorem mvPolynomialBasis_repr_symm_single (σ) (i) (x) :
    (mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • D R (MvPolynomial σ R) (.X i) := by
  apply (mvPolynomialBasis R σ).repr.injective; simp [LinearEquiv.map_smul, -map_smul]

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