reducing imports to algebra.invertible

Stream: PR reviews

[Scott Morrison]

Mario asked for algebra.invertible to be ported, to support tactics in mathlib4. PRs #17174, #17175, #17176 all reduce the import requirements for algebra.invertible, so that can happen sooner.

(These PRs will have interactions, requiring imports to be rearranged downstream, so if they could be delegated rather than merged that would be great.)