Theorem Matrix.add_mul_mul_inv_eq_sub'

Modification history

2025-11-12 00:55
Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
feat(Data.Matrix.Invertible): the binomial inverse theorem (#31507) …
Added Matrix.add_mul_mul_inv_eq_sub'View on Github →