Commit 2020-08-05 16:34 5fc62815

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.