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_basisView 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)
Modified equiv_of_is_basisView on Github →2019-10-10 11:14
src/linear_algebra/basis.lean
chore(linear_algebra): rename type variables (#1521) …
Modified equiv_of_is_basisView on Github →2019-07-03 09:42
src/linear_algebra/basis.lean
refactor(linear_algebra/lc): use families not sets (#943) …
Modified equiv_of_is_basisView on Github →