Theorems · Theorem · linear algebra

Matrix.det_piecewise_one_eq_submatrix_det

∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R)
  (s : Finset n), (Matrix.of (s.piecewise M.row (Matrix.row 1))).det = (M.submatrix Subtype.val Subtype.val).det

The determinant of the matrix obtained by replacing rows outside s with identity rows equals the determinant of the principal submatrix indexed by s.

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEqFintype