det_reindex_self — Mathlib

English

Reindexing both indices along an equivalence e preserves the determinant: det(A.submatrix e e) = det A.

Русский

Переиндексация обеих индексов по эквиваленсу e сохраняет детерминант: det(A.submatrix e e) = det A.

LaTeX

$$$$\det(A_{e,e}) = \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`; this one is unsuitable because
`Matrix.reindex_apply` unfolds `reindex` first.
-/
theorem det_reindex_self (e : m ≃ n) (A : Matrix m m R) : det (reindex e e A) = det A :=
  det_submatrix_equiv_self e.symm A

Похожие утверждения