mathlib3

d5c2cdaf - feat(data/matrix/basic): promote subsingleton instances to unique instances