Commit 2024-01-04 22:32 02d418dd

View on Github →

chore: Move MulOpposite.op_pow (#9442) These lemmas can actually be proved much earlier than they were. Part of #9411

Estimated changes

Modified Mathlib/Algebra/Group/Opposite.lean

added theorem MulOpposite.op_pow

added theorem MulOpposite.op_zpow

added theorem MulOpposite.unop_pow

added theorem MulOpposite.unop_zpow

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

deleted theorem MulOpposite.op_pow

deleted theorem MulOpposite.op_zpow

deleted theorem MulOpposite.unop_pow

deleted theorem MulOpposite.unop_zpow