Theorems · Theorem · linear algebra

Matrix.det_reindex_self

∀ {m : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] {R : Type v} [inst_4 : CommRing R] (e : m ≃ n) (A : Matrix m m R),
  ((Matrix.reindex e e) A).det = A.det

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.

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Cited by

22 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeDecidableEqFintypeCommRing