Theorem Matrix.add_mul_mul_mul_invOf_eq_one

Modification history

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