mathlib

b54f44f0 - feat(data/matrix/notation): expansions of matrix multiplication for 2x2 and 3x3 (#12088)

feat(data/matrix/notation): expansions of matrix multiplication for 2x2 and 3x3 (#12088) A clever way to generalize this would be to make a recursivedefinition of `mul` and `one` that's defeq to the desired `![...]` result and prove that's equal to the usual definition, but that doesn't help with actually writing the lemma statement, which is the tedious bit.