piRightHom_tmul

Mathlib.LinearAlgebra.TensorProduct.Pi

URI: https://scilib.ai/kg/mathlib#TensorProduct.piRightHom_tmul

English

For a ∈ A and b ∈ B, (opAlgEquiv).symm (op (a ⊗ b)) = a^{op} ⊗ b^{op}.

Русский

Для a ∈ A и b ∈ B, ((opAlgEquiv).symm) (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 piRightHom_tmul (x : N) (f : ∀ i, M i) : piRightHom R S N M (x ⊗ₜ f) = (fun j ↦ x ⊗ₜ f j) :=
  rfl

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

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

Разделы

Аффилиация

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