Theorems · Theorem · linear algebra

Matrix.det_submatrix_equiv_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 : n ≃ m) (A : Matrix m m R),
  (A.submatrix ⇑e ⇑e).det = A.det

Permuting rows and columns with the same equivalence does not change the determinant.

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidableEqFintypeCommRing