Commit 2022-01-18 09:14 f23c00f2
View on Github →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.