rTensor_symm_apply_single — Mathlib

English

The symmetric form rTensor.symm sends Finsupp.single d (s ⊗ n) back to (monomial d s) ⊗ n.

Русский

Симметрическая карта rTensor.symm отправляет Finsupp.single d (s ⊗ n) в (monomial d s) ⊗ n.

LaTeX

$$$rTensor.symm (\\mathrm{Finsupp}.single d (s \\otimes n)) = (\\mathrm{monomial}\\; d\\; s) \\otimes n$$$

Lean4

@[simp]
theorem rTensor_symm_apply_single (d : σ →₀ ℕ) (s : S) (n : N) :
    rTensor.symm (Finsupp.single d (s ⊗ₜ n)) = (monomial d s) ⊗ₜ[R] n :=
  TensorProduct.finsuppLeft_symm_apply_single (R := R) d s n

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