mathlib
24ce416a
- chore(data/matrix/basic): clean up of new lemmas on matrix numerals (#2996)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(data/matrix/basic): clean up of new lemmas on matrix numerals (#2996) Generalise and improve use of `@[simp]` for some newly added lemmas about matrix numerals. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
kim-em
Parents
7bb2d89f
Loading