invOf_add_mul_mul — Mathlib

English

Let A and C be invertible square matrices of sizes n×n and m×m, respectively, and let U and V be n×m and m×n matrices over a ring. If A + U C V is invertible, then

Русский

Пусть A и C — обратимые квадратные матрицы размерности n×n и m×m соответственно, а U и V — матрицы над кольцом размерности n×m и m×n. Если A + U C V обратима, то

LaTeX

$$$\displaystyle (A + U C V)^{-1} = A^{-1} - A^{-1} U \,(C^{-1} + V A^{-1} U)^{-1} V A^{-1}$$$

Lean4

/-- The **Woodbury Identity** (`⅟` version). -/
theorem invOf_add_mul_mul [Invertible (A + U * C * V)] : ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A :=
  by
  letI := invertibleAddMulMul A U C V
  convert (rfl : ⅟(A + U * C * V) = _)

Похожие утверждения