Commit 2021-11-22 11:23 d8d0c595

chore(algebra/opposites): split group actions and division_ring into their own files (#10383) This splits out group_theory.group_action.opposite and algebra.field.opposite from algebra.opposites. The motivation is to make opposite actions available slightly earlier in the import graph. We probably want to split out ring at some point too, but that's likely a more annoying change so I've left it for future work. These lemmas are just moved, and some _root_ prefixes eliminated by removing the surrounding namespace.