Theorems · Theorem · linear algebra

Matrix.det_succ_column_zero

∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R),
  A.det = ∑ i, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Laplacian expansion of the determinant of an n+1 × n+1 matrix along column 0.

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing