Theorems · Theorem · linear algebra

Matrix.detp_submatrix_equiv_equiv

∀ {n : Type u_1} {m : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommSemiring R] (s : ℤˣ) (A : Matrix n n R) (f g : m ≃ n),
  Matrix.detp s (A.submatrix ⇑f ⇑g) = Matrix.detp (s * Equiv.Perm.sign (f.symm.trans g)) A

Defined in

Mathlib.LinearAlgebra.Matrix.SemiringInverse

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeFintypeDecidableEqDecidableEqCommSemiring