opAlgEquiv_tmul

Mathlib.LinearAlgebra.TensorProduct.Opposite

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

English

On simple tensors a^{op} ⊗ b^{op}, the isomorphism sends to (a.unop ⊗ b.unop)^{op}.

Русский

На простых тензорах a^{op} ⊗ b^{op} изоморфизм отправляет в (a.unop ⊗ b.unop)^{op}.

LaTeX

$$$opAlgEquiv_R S A B\,(a^{op} \otimes b^{op}) = (a^{unop} \otimes b^{unop})^{op}.$$$

Lean4

@[simp]
theorem opAlgEquiv_tmul (a : Aᵐᵒᵖ) (b : Bᵐᵒᵖ) : opAlgEquiv R S A B (a ⊗ₜ[R] b) = op (a.unop ⊗ₜ b.unop) :=
  rfl

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

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

Разделы

Аффилиация

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