feat(algebra/invertible): lemmas (#3493)
feat(algebra/invertible): lemmas (#3493)

Coauthored by: Johan Commelin <johan@commelin.net>


Co-authored-by: Rob Lewis <597e2d195b18d1f0b2b6530cee088a0ab0ed3ce2@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib