Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv_of_is_basis_comp

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_compView on Github →
2020-08-20 23:05
src/linear_algebra/basis.lean
feat(linear_algebra): some easy linear map/equiv lemmas (#3890) …
Added equiv_of_is_basis_compView on Github →