Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv_of_is_basis'

Modification history

2021-01-02 10:18
src/linear_algebra/basis.lean
feat(linear_algebra/dimension): linear equiv iff eq dim (#5559) …
Deleted equiv_of_is_basis'View 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 equiv_of_is_basis'View on Github →