English
If A, C are invertible and (C^{-1} + V A^{-1} U) is invertible, then A + U C V is invertible and its inverse is the explicit block formula; moreover, the two block-product equalities hold.
Русский
Если A и C обратимы и (C^{-1} + V A^{-1} U) обратима, то A + U C V обратима и её обратная матрица дана явной блочной формулой; при этом выполняются обе тождественные блок-умножения.
LaTeX
$$$\text{Invertible}(A) \land \text{Invertible}(C) \land \text{Invertible}(\,\tfrac{1}{C} + V \tfrac{1}{A} U) \Rightarrow \text{Invertible}(A + U C V)$ with $ (A + U C V)^{-1} = \tfrac{1}{A} - \tfrac{1}{A} U \tfrac{1}{(\tfrac{1}{C} + V \tfrac{1}{A} U)} V \tfrac{1}{A}$$$
Lean4
/-- If matrices `A`, `C`, and `C⁻¹ + V * A⁻¹ * U` are invertible, then so is `A + U * C * V`. -/
def invertibleAddMulMul : Invertible (A + U * C * V)
where
invOf := ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A
invOf_mul_self := add_mul_mul_invOf_mul_eq_one' _ _ _ _
mul_invOf_self := add_mul_mul_invOf_mul_eq_one _ _ _ _
