mathlib3

ad4040dd - feat(algebra/opposites): provide npow and gpow explicitly, prove `op_gpow` and `unop_gpow` (#9659)

feat(algebra/opposites): provide npow and gpow explicitly, prove `op_gpow` and `unop_gpow` (#9659) By populating the `npow` and `gpow` fields in the obvious way, `op_pow` and `unop_pow` are true definitionally. This adds the new lemmas `op_gpow` and `unop_gpow` which works for `group`s and `division_ring`s too. Note that we do not provide an explicit `div` in `div_inv_monoid`, because there is no "reversed division" operator to define it via. This also reorders the lemmas so that the definitional lemmas are available before any proof obligations might appear in stronger typeclasses.