Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-10 05:42 47264da1

View on Github →

feat(linear_algebra): tiny missing pieces (#4089) From the sphere eversion project.

Estimated changes

Modified src/linear_algebra/basic.lean

added def linear_map.applyₗ

Modified src/linear_algebra/finite_dimensional.lean

added theorem finite_dimensional.equiv_fin

added theorem finite_dimensional.fin_basis