Commit 2024-09-26 03:24 facf1f9c

View on Github →

feat(LinearAlgebra/Matrix): Woodbury Identity (#16325) This adds the Woodbury Identity. Zulip discussion Also corrects some bad deprecations introduced in #16590, which affected development of this PR.

Estimated changes

Modified Mathlib/Data/Matrix/Invertible.lean

added theorem Matrix.add_mul_mul_invOf_mul_eq_one'

added theorem Matrix.add_mul_mul_invOf_mul_eq_one

added theorem Matrix.invOf_add_mul_mul

added def Matrix.invertibleAddMulMul

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.add_mul_mul_inv_eq_sub