theorem
TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_eq_swap_middle_tensor
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
{D : Type u_5}
[CommSemiring R]
[AddCommMonoid A]
[AddCommMonoid B]
[AddCommMonoid C]
[AddCommMonoid D]
[Module R A]
[Module R B]
[Module R C]
[Module R D]
:
theorem
TensorProduct.map_schurMul
{A : Type u_1}
{B : Type u_2}
{C : Type u_3}
{D : Type u_4}
[AddCommMonoid A]
[Semiring B]
[AddCommMonoid C]
[Semiring D]
[Module ℂ A]
[Module ℂ B]
[Module ℂ C]
[Module ℂ D]
[Coalgebra ℂ A]
[Coalgebra ℂ C]
[SMulCommClass ℂ B B]
[SMulCommClass ℂ D D]
[IsScalarTower ℂ B B]
[IsScalarTower ℂ D D]
{f h : A →ₗ[ℂ] B}
{g k : C →ₗ[ℂ] D}
: