mathlib

8f9c10fc - feat(data/matrix): add `matrix.mul_sub` and `matrix.sub_mul` (#4505)

feat(data/matrix): add `matrix.mul_sub` and `matrix.sub_mul` (#4505) I was quite surprised that we didn't have this yet, but I guess they weren't needed when `sub_eq_add_neg` was still `@[simp]`.