Theorems · Theorem · linear algebra

Matrix.add_mul_mul_inv_eq_sub

∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α)
  (V : Matrix m n α),
  IsUnit A → IsUnit C → IsUnit (C⁻¹ + V * A⁻¹ * U) → (A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹

The Woodbury Identity (⁻¹ version). See add_mul_mul_inv_eq_sub' for the binomial inverse theorem.

Defined in

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRingFintypeDecidableEq