piRight_symm_apply — Mathlib

English

The inverse map on simple tensors is given by the canonical factorwise operation.

Русский

Обратное отображение на простых тензорах задаётся каноническим пофакторному действию.

LaTeX

$$$ (opAlgEquiv R S A B)^{-1} (a^{op} \otimes b^{op}) = a \otimes b^{op}. $$$

Lean4

@[simp]
theorem piRight_symm_apply (x : N) (m : ∀ i, M i) : (piRight R S N M).symm (fun i ↦ x ⊗ₜ m i) = x ⊗ₜ m := by
  simp [piRight]

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