Mathlib v3 is deprecated. Go to Mathlib v4

Def matrix.reindex_linear_equiv

Modification history

2021-07-05 10:29
src/linear_algebra/matrix/reindex.lean
feat(linear_algebra/matrix/reindex): generalize reindex_linear_equiv to operate on an arbitrary ring (#8159) …
Modified matrix.reindex_linear_equivView on Github →
2021-05-15 14:21
src/linear_algebra/matrix.lean
refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) …
Modified matrix.reindex_linear_equivView on Github →
2020-07-18 09:27
src/linear_algebra/matrix.lean
feat(linear_algebra/matrix): define equivalences for reindexing matrices with equivalent types (#3409)
Added matrix.reindex_linear_equivView on Github →