mathlib

ce332c11 - refactor(algebra/group_power): split ring lemmas into a separate file (#15032)

refactor(algebra/group_power): split ring lemmas into a separate file (#15032) This doesn't actually stop `algebra.ring.basic` being imported into `group_power.basic` yet, but it makes it easier to make that change in future. Two ~300 line files are also slightly easier to manage than one ~600 line file, and ring/add_group feels like a natural place to draw the line All lemmas have just been moved, and none have been renamed. Some lemmas have had their `R` variables renamed to `M` to better reflect that they apply to monoids with zero. By grouping together the `monoid_with_zero` lemmas from separate files, it become apparent that there's some overlap. This PR does not attempt to clean this up, in the interest of limiting the the scope of this change to just moves.