mathlib
5fc62815 - chore(data/matrix/basic): rename _val lemmas to _apply (#3297)

Commit
5 years ago
chore(data/matrix/basic): rename _val lemmas to _apply (#3297) We use `_apply` for lemmas about applications of functions to arguments. Arguably "picking out the entries of a matrix" could warrant a different name, but as we treat matrices just as functions all over, I think it's better to use the usual names. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
Parents
Loading