English
Determinant is preserved under simultaneous reindexing by any equivalence for matrices over a ring B with R-algebra structure: det(reindexAlgEquiv R B e A) = det A.
Русский
Определитель сохраняется при одновременной реиндексации по любой эквивалентности для матриц над кольцом B с алгебраическим связыванием с R: det(reindexAlgEquiv R B e A) = det A.
LaTeX
$$$ \det(\mathrm{reindexAlgEquiv}\ R\ B\ e\ A) = \det A $$$
Lean4
/-- Reindexing both indices along the same equivalence preserves the determinant.
For the `simp` version of this lemma, see `det_submatrix_equiv_self`.
-/
theorem det_reindexAlgEquiv (B : Type*) [CommSemiring R] [CommRing B] [Algebra R B] [Fintype m] [DecidableEq m]
[Fintype n] [DecidableEq n] (e : m ≃ n) (A : Matrix m m B) : det (reindexAlgEquiv R B e A) = det A :=
det_reindex_self e A
