mathlib

f23c00f2 - chore(algebra/order/ring): move lemmas about invertible into a new file (#11511)

chore(algebra/order/ring): move lemmas about invertible into a new file (#11511) The motivation here is to eventually be able to use the `one_pow` lemma in `algebra.group.units`. This is one very small step in that direction.