# Documentation

Mathlib.LinearAlgebra.TensorProduct.Opposite

# MulOpposite distributes over ⊗#

The main result in this file is:

• Algebra.TensorProduct.opAlgEquiv R S A B : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ
def Algebra.TensorProduct.opAlgEquiv (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [] :

MulOpposite distributes over TensorProduct. Note this is an S-algebra morphism, where A/S/R is a tower of algebras.

Instances For
theorem Algebra.TensorProduct.opAlgEquiv_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [] (x : ) :
↑() x = MulOpposite.op (↑() x)
theorem Algebra.TensorProduct.opAlgEquiv_symm_apply (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [] (x : ()ᵐᵒᵖ) :
↑() x =
@[simp]
theorem Algebra.TensorProduct.opAlgEquiv_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [] (a : Aᵐᵒᵖ) (b : Bᵐᵒᵖ) :
↑() (a ⊗ₜ[R] b) =
@[simp]
theorem Algebra.TensorProduct.opAlgEquiv_symm_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [] [] [] [] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [] (a : A) (b : B) :
↑() (MulOpposite.op (a ⊗ₜ[R] b)) =