Commit 2021-10-12 08:59 ad4040dd

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 groups and division_rings 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.