mathlib

c9704ff5 - chore(data/matrix, linear_algebra): generalize universe parameters (#3879)

chore(data/matrix, linear_algebra): generalize universe parameters (#3879) @PatrickMassot was complaining that `matrix m n R` often doesn't work when the parameters are declared as `m n : Type*` because the universe parameters were equal. This PR makes the universe parameters of `m` and `n` distinct where possible, also generalizing some other linear algebra definitions. The types of `col` and `row` used to be `matrix n punit` but are now `matrix n unit`, otherwise the elaborator can't figure out the universe. This doesn't seem to break anything except for the cases where `punit.{n}` was explicitly written down. There were some breakages, but the total amount of changes is not too big. Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>