Theorem matrix.reindex_linear_equiv_mul
Modification history
2021-08-26 13:06
src/linear_algebra/matrix/reindex.lean
feat(*): remove the `fintype` requirement from matrices. (#8810) …
Modified matrix.reindex_linear_equiv_mulView on Github →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_equiv_mulView on Github →