piScalarRight_symm_single — Mathlib

English

The symmetrized right-scalar action on a simple tensor x at index i yields x ⊗ₜ Pi.single i 1; more precisely, the inverse of the pi-scalar-right map sends Pi.single i x to x ⊗ₜ Pi.single i 1.

Русский

Двойственное правое скалярное действие на простом тензоре в индексе i даёт x ⊗ₜ Pi.single i 1; точнее, обратное отображение piScalarRight отправляет Pi.single i x в x ⊗ₜ Pi.single i 1.

LaTeX

$$$(\\piScalarRight\,R\,S\,N\,\\iota)^{-1}(\\Pi_{i} x) = x \\otimes_\\mathrm{t} \\Pi_{i} 1$$$

Lean4

@[simp]
theorem piScalarRight_symm_single (x : N) (i : ι) : (piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ Pi.single i 1 :=
  by simp [piScalarRight]

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