mathlib3
094b1f51
- chore(*/matrix): order `m` and `n` alphabetically (#13510)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
chore(*/matrix): order `m` and `n` alphabetically (#13510) In a few places this also reorders `(n) [fintype n] (m) [fintype m]` to `(m n) [fintype m] [fintype n]` which seems to be where we prefer to put typeclasses.
Author
eric-wieser
Parents
3ac979a2
Loading