mathlib
f63069f3 - feat(linear_algebra/basic): simp lemmas about endomorphisms (#6452)

Commit
5 years ago
feat(linear_algebra/basic): simp lemmas about endomorphisms (#6452) Also renames some lemmas: * `linear_map.one_app` has been renamed to `linear_map.one_apply` * `linear_map.mul_app` has been removed in favour of the existing `linear_map.mul_app`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading