English
A mirrored version of the block inverse identity, giving the reversed product with the same hypotheses, also equaling the identity.
Русский
Зеркальное утверждение идентичности обратного блока с теми же гипотезами, дающее обратную матрицу через обратную последовательность операций.
LaTeX
$$We have the reversed block identity: $(\tfrac{1}{A} - \tfrac{1}{A} U (\tfrac{1}{C} + V \tfrac{1}{A} U)^{-1} V \tfrac{1}{A}) (A + U C V) = I$$$
Lean4
/-- Like `add_mul_mul_invOf_mul_eq_one`, but with multiplication reversed. -/
theorem add_mul_mul_invOf_mul_eq_one' : (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) * (A + U * C * V) = 1 := by
calc
(⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) * (A + U * C * V)
_ =
⅟A * A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * A + ⅟A * U * C * V -
⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V :=
by simp_rw [add_sub_assoc, _root_.mul_add, _root_.sub_mul, Matrix.mul_assoc]
_ = (1 + ⅟A * U * C * V) - (⅟A * U * ⅟(⅟C + V * ⅟A * U) * V + ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V) :=
by
rw [invOf_mul_self, Matrix.invOf_mul_cancel_right]
abel
_ = 1 + ⅟A * U * C * V - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * (V + V * ⅟A * U * C * V) :=
by
rw [sub_right_inj, Matrix.mul_add]
simp_rw [Matrix.mul_assoc]
_ = 1 + ⅟A * U * C * V - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * (⅟C + V * ⅟A * U) * C * V :=
by
congr 1
simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc, Matrix.invOf_mul_cancel_right]
_ = 1 := by
rw [Matrix.invOf_mul_cancel_right]
abel
