Documentation

Monlib.LinearAlgebra.QuantumSet.schurMulTensor

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} :
map f g •ₛ map h k = map (f •ₛ h) (g •ₛ k)