Documentation

Mathlib.LinearAlgebra.TensorProduct.Opposite

MulOpposite distributes over #

The main result in this file is:

noncomputable def Algebra.TensorProduct.opAlgEquiv (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] :

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Algebra.TensorProduct.opAlgEquiv_symm_tmul (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [IsScalarTower R S A] (a : A) (b : B) :