mathlib

d8d0c595 - chore(algebra/opposites): split group actions and division_ring into their own files (#10383)

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`.