Theorems · Theorem · linear algebra

Matrix.det_reindexAlgEquiv

∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (B : Type u_13) [inst : CommSemiring R] [inst_1 : CommRing B]
  [inst_2 : Algebra R B] [inst_3 : Fintype m] [inst_4 : DecidableEq m] [inst_5 : Fintype n] [inst_6 : DecidableEq n]
  (e : m ≃ n) (A : Matrix m m B), ((Matrix.reindexAlgEquiv R B 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.

Defined in

Mathlib.LinearAlgebra.Matrix.Reindex

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommRingAlgebraFintypeDecidableEqFintypeDecidableEq