Commit 2021-03-02 02:22 f63069f3
View on Github →feat(linear_algebra/basic): simp lemmas about endomorphisms (#6452) Also renames some lemmas:
linear_map.one_app
has been renamed tolinear_map.one_apply
linear_map.mul_app
has been removed in favour of the existinglinear_map.mul_app
.