Mathlib v3 is deprecated. Go to Mathlib v4

Theorem opposite.op_pow

Modification history

2021-11-19 12:03
src/algebra/group_power/lemmas.lean
refactor(algebra/opposites): use mul_opposite for multiplicative opposite (#10302) …
Deleted opposite.op_powView on Github →
2021-10-12 08:59
src/algebra/group_power/lemmas.lean
feat(algebra/opposites): provide npow and gpow explicitly, prove `op_gpow` and `unop_gpow` (#9659) …
Modified opposite.op_powView on Github →
2021-06-28 06:13
src/algebra/group_power/lemmas.lean
fix(algebra/group_power): put opposite lemmas in the right namespace (#8100)
Added opposite.op_powView on Github →