mathlib3

f54f81c0 - refactor(algebra/invertible): push deeper into the import graph (#6650)

refactor(algebra/invertible): push deeper into the import graph (#6650) I want to be able to import this in files where we use `is_unit`, to remove a few unecessary non-computables. This moves all the lemmas about `char_p` and `char_zero` from `algebra.invertible` to `algebra.char_p.invertible`. This means that we can talk about `invertible` elements without having to build up the theory in `order_of_element` first. This doesn't change any lemma statements or proofs, but it does move some type arguments into `variables` statements.