mathlib3

feat(data/matrix/basic): use `⬝` as notation for all products

#15585

Open