Theorems · Theorem · linear algebra

Matrix.det_add_mul

∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] {A : Matrix m m α} (U : Matrix m n α) (V : Matrix n m α),
  IsUnit A.det → (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

A generalization of the Matrix determinant lemma

Defined in

Mathlib.LinearAlgebra.Matrix.SchurComplement

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFintypeDecidableEqDecidableEqCommRing