Matrix.det_reindexLinearEquiv_self
theorem Matrix.det_reindexLinearEquiv_self :
∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
[inst_3 : Fintype n] [inst_4 : DecidableEq n] (e : m ≃ n) (M : Matrix m m R),
((Matrix.reindexLinearEquiv R R e e) M).det = M.det
This theorem, `Matrix.det_reindexLinearEquiv_self`, states that for any given type `m`, type `n`, and type `R` (where `R` is a commutative ring), if both indices of a matrix `M` with entries of type `R` and indices of type `m` are reindexed along the same equivalence `e` between `m` and `n`, the determinant of the reindexed matrix is the same as the determinant of the original matrix. This is true when `m` and `n` are finite types with decidable equality.
More concisely: For any commutative ring R and finite types m and n with decidable equality, the determinant of a matrix over R with reindexed indices along an equivalence e between m and n is equal to the determinant of the originally indexed matrix.
|
Matrix.det_reindexAlgEquiv
theorem Matrix.det_reindexAlgEquiv :
∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
[inst_3 : Fintype n] [inst_4 : DecidableEq n] (e : m ≃ n) (A : Matrix m m R),
((Matrix.reindexAlgEquiv R e) A).det = A.det
This theorem states that for any two types `m` and `n`, and a type `R` that is a commutative ring, given a bijective map `e` from `m` to `n` and a square matrix `A` of type `m` with entries in `R`, the determinant of the matrix `A` after reindexing both its row and column indices along the equivalence `e` using `Matrix.reindexAlgEquiv` is equal to the original determinant of `A`. In simpler terms, it says that changing the labels of the rows and columns of a square matrix does not change its determinant. Both `m` and `n` need to be finite types and have decidable equality for this theorem to hold.
More concisely: The determinant of a square matrix is unchanged when its rows and columns are reindexed via a bijective map between their finite, decidably-equaled types.
|