Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.std_basis_eq_pi_diag

Modification history

2021-02-20 01:44
src/linear_algebra/std_basis.lean
refactor(linear_algebra/pi): add `linear_map.single` to match `add_monoid_hom.single` (#6315) …
Added linear_map.std_basis_eq_pi_diagView on Github →