Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-19 08:28 3968f7f4

View on Github →

feat(linear_algebra): equiv_of_is_basis' and module.fintype_of_fintype (#2735)

Estimated changes

Modified src/linear_algebra/basis.lean

added def equiv_of_is_basis'

modified def equiv_of_is_basis

added def module.fintype_of_fintype