English
The equivalence between invertible diagonals and invertible vectors is established by two maps: diagonalInvertible and invertibleOfDiagonalInvertible, each serving as a quasi-inverse to the other.
Русский
Эквивалентность между обратимостью диагональных матриц и обратимостью векторов устанавливается двумя отображениями: diagonalInvertible и invertibleOfDiagonalInvertible, образующими пары взаимно обратных.
LaTeX
$$diagonalInvertibleEquivInvertible(v) : Invertible(diagonal v) ≃ Invertible v$$
Lean4
/-- The **Woodbury Identity** (`⁻¹` version). -/
theorem add_mul_mul_inv_eq_sub (hA : IsUnit A) (hC : IsUnit C) (hAC : IsUnit (C⁻¹ + V * A⁻¹ * U)) :
(A + U * C * V)⁻¹ = A⁻¹ - A⁻¹ * U * (C⁻¹ + V * A⁻¹ * U)⁻¹ * V * A⁻¹ :=
by
obtain ⟨_⟩ := hA.nonempty_invertible
obtain ⟨_⟩ := hC.nonempty_invertible
obtain ⟨iAC⟩ := hAC.nonempty_invertible
simp only [← invOf_eq_nonsing_inv] at iAC
letI := invertibleAddMulMul A U C V
simp only [← invOf_eq_nonsing_inv]
apply invOf_add_mul_mul
