Commit 2022-07-01 08:11 ce332c11

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.