Theorems · Theorem · linear algebra

Matrix.det_succ_column

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

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

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing