mathlib3

6c351a8f - refactor(data/matrix/basic): add matrix.of for type casting (#14992)

refactor(data/matrix/basic): add matrix.of for type casting (#14992) Without this, it is easier to get confused between matrix and pi types, which have different multiplication operators. With this in place, we can have a special matrix notation that actually produces terms of type `matrix`.