Mathlib v3 is deprecated. Go to Mathlib v4

Def module.fintype_of_fintype

Modification history

2023-01-22 01:07
src/linear_algebra/basis.lean
fix(linear_algebra/basis): add missing decidable arguments in lemmas (#18252) …
Modified module.fintype_of_fintypeView on Github →
2020-05-19 08:28
src/linear_algebra/basis.lean
feat(linear_algebra): equiv_of_is_basis' and module.fintype_of_fintype (#2735)
Added module.fintype_of_fintypeView on Github →