mathlib3

b9e4c084 - refactor(algebra/regular): split out `is_regular` (#8561)

refactor(algebra/regular): split out `is_regular` (#8561) One would like to import `is_regular` for rings. However, group powers are too late in the algebra hierarchy, so the proofs of powers of regular elements are factored out to a separate file.