In a recent PR #10238 it was suggested that mathlib should have a namespace for bilinear maps and add an abbrev BilinearMap := M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P in order to support dot-notation.