opAlgEquiv_symm_tmul

Mathlib.LinearAlgebra.TensorProduct.Opposite

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.opAlgEquiv_symm_tmul

English

The inverse map sends op(a ⊗ b) back to a^{op} ⊗ b^{op}.

Русский

Обратное отображение возвращает op(a ⊗ b) к a^{op} ⊗ b^{op}.

LaTeX

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

Lean4

@[simp]
theorem opAlgEquiv_symm_tmul (a : A) (b : B) : (opAlgEquiv R S A B).symm (op <| a ⊗ₜ[R] b) = op a ⊗ₜ op b :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru