mathlib

ef5d936c - chore(algebra/invertible): weaken typeclass requirements for `invertible.of_left_inverse` (#17267)