Commit 2024-06-11 13:49 bfaec997
View on Github →feat: generalize one_div_mul_add_mul_one_div_eq_one_div_add_one_div (#13215)
This provides a variant that works on invertible elements of semirings, via invOf and Ring.inverse
This lets this be used on matrices.
The original lemma is from https://github.com/leanprover/lean3/commit/816c315b501481cea4edae1f9eecbd05c554fb61.