mathlib
9af7e5b5 - refactor(linear_algebra/basic): use smul_right (#1640)

Commit
6 years ago
refactor(linear_algebra/basic): use smul_right (#1640) * refactor(linear_algebra/basic): use smul_right * Update src/linear_algebra/basic.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/linear_algebra/basic.lean Co-Authored-By: Scott Morrison <scott@tqft.net>
Author
Committer
Parents
Loading