Commit 2021-02-20 01:44 32b9b214
View on Github →refactor(linear_algebra/pi): add linear_map.single to match add_monoid_hom.single (#6315)
This changes the definition of std_basis to be exactly linear_map.single, but proves equality with the old definition.
In future, it might make sense to remove std_basis entirely.