Mathlib v3 is deprecated. Go to Mathlib v4

Def finite_dimensional.fintype_basis_index

Modification history

2021-10-25 17:42
src/linear_algebra/finite_dimensional.lean
refactor(linear_algebra/finite_dimensional): define finite_dimensional using module.finite (#9854) …
Added finite_dimensional.fintype_basis_indexView on Github →