det_reindexLinearEquiv_self — Mathlib

English

Determinant is invariant under simultaneous reindexing of both indices along the same equivalence: det(reindexLinearEquiv R R e e M) = det M.

Русский

Определитель инвариант при одновременной реиндексации обеих осей по одной и той же эквивалентности: det(reindexLinearEquiv R R e e M) = det M.

LaTeX

$$$ \det(\mathrm{reindexLinearEquiv}\ R\ R\ e\ e\ M) = \det M $$$

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_reindexLinearEquiv_self [CommRing R] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (e : m ≃ n)
    (M : Matrix m m R) : det (reindexLinearEquiv R R e e M) = det M :=
  det_reindex_self e M

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