Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
linear_map.coe_std_basis
Modification history
2021-02-17 11:38
src/linear_algebra/std_basis.lean
feat(linear_algebra/pi): ext lemma for `f : (Π i, M i) →ₗ[R] N` (#6233)
Added
linear_map.coe_std_basis
View on Github →