Algebraic structure underlying multiplication of matrices

Stream: mathlib4

[Antoine Chambert-Loir]

Some matrix identities such as the Woodbury identity docs#Matrix.invertibleAddMulMul are not at all specific to matrices but require a kind of structure, in which we have a bunch of heterogeneous bilinear multiplications.
I wonder what this structure would be. (This is related to the rather elementary PR #31507)

The multiplications can be defined using docs#HMul but there doesn't seem to be anything such as distributivity for hetereogeneous multiplications.

[Eric Wieser]

I fear that this also requires developing HMulAssoc, HMulOneClass etc

[Antoine Chambert-Loir]

Could bimodules do the job? (but I would like a HMul-like notation rather than smul). (No : that's still missing the $(n\times p, p\times n)$ multiplication of matrices.)

[Jireh Loreaux]

When reviewing this PR, I considered that there was nothing truly matrix specific, but then merged it anyway for exactly the reason that we don't currently have any unifying type classes for this. Indeed, to my knowledge, there are exactly two heterogeneous mul/smul classes in Mathlib: Matrix and MeasureTheory.Lp. These each have their own dedicated API for the heterogeneity. If we managed to find a third, I was going to consider doing the generalization.