Commit 2025-05-27 21:21 6569c4c3

feat(LinearAlgebra): generalize TensorTensorTensorComm (#25216)

• Generalize LinearMap.lflip to flip heterobasic bilinear maps (M →ₗ[R] N →ₗ[A] P).
• Generalize LinearMap.lcomp to be "more linear"
• Generalize Algebra.TensorProduct.rightComm to

  (M ⊗ˢ P)      ⎛ M ⎞ ⊗ˢ P
   ⊗ᴿ       ≅ᴮ  ⎜ ⊗ᴿ⎟
   Q            ⎝ Q ⎠
  

  for a diagram of algebras R → B ← S, and a B-module M, S-module P, R-module Q.
• Generalize Algebra.TensorProduct.tensorTensorTensorComm to

  (M ⊗ˢ N)      ⎛ M ⎞ ⊗ˢ ⎛ N ⎞
   ⊗ᴬ       ≅ᴮ  ⎜ ⊗ᴬ⎟    ⎜ ⊗ᴿ⎟
  (P ⊗ᴿ Q)      ⎝ P ⎠    ⎝ Q ⎠
  

  for towers of algebras R → S → B and R → A → B, and a B-module M, S-module N, A-module P, R-module Q.