English
Permuting rows and columns by two equivalences e1,e2 does not change the absolute value of the determinant: |det(A.submatrix e1 e2)| = |det A|.
Русский
Перестановка строк и столбцов двумя эквивалентностями e1,e2 не меняет модуль детерминанта: |det(A.submatrix e1 e2)| = |det A|.
LaTeX
$$$$\left|\det\left(A_{e_1,e_2}\right)\right| = \left|\det A\right|$$$$
Lean4
/-- Reindexing both indices along equivalences preserves the absolute of the determinant.
For the `simp` version of this lemma, see `abs_det_submatrix_equiv_equiv`;
this one is unsuitable because `Matrix.reindex_apply` unfolds `reindex` first.
-/
theorem abs_det_reindex {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (e₁ e₂ : m ≃ n)
(A : Matrix m m R) : |det (reindex e₁ e₂ A)| = |det A| :=
abs_det_submatrix_equiv_equiv e₁.symm e₂.symm A
