Changing the index type of a matrix #
This file concerns the map Matrix.reindex
, mapping a m
by n
matrix
to an m'
by n'
matrix, as long as m ≃ m'
and n ≃ n'
.
Main definitions #
Matrix.reindexLinearEquiv R A
:Matrix.reindex
is anR
-linear equivalence betweenA
-matrices.Matrix.reindexAlgEquiv R
:Matrix.reindex
is anR
-algebra equivalence betweenR
-matrices.
Tags #
matrix, reindex
The natural map that reindexes a matrix's rows and columns with equivalent types,
Matrix.reindex
, is a linear equivalence.
Instances For
For square matrices with coefficients in commutative semirings, the natural map that reindexes
a matrix's rows and columns with equivalent types, Matrix.reindex
, is an equivalence of algebras.
Instances For
Reindexing both indices along the same equivalence preserves the determinant.
For the simp
version of this lemma, see det_submatrix_equiv_self
.
Reindexing both indices along the same equivalence preserves the determinant.
For the simp
version of this lemma, see det_submatrix_equiv_self
.