mathlib3

32b9b214 - refactor(linear_algebra/pi): add `linear_map.single` to match `add_monoid_hom.single` (#6315)

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.