Commit 2022-12-12 02:05 c37887cc

View on Github →

feat: port algebra.group.opposite (#912) Based off Mathlib3 SHA: 655994e298904d7e5bbd1e18c95defd7b543eb94

Estimated changes

added def AddEquiv.mulOp
added def AddEquiv.mulUnop
added def AddHom.mulOp
added def AddHom.mulUnop
added theorem AddOpposite.op_pow
added theorem AddOpposite.unop_pow
added theorem Commute.op
added def MonoidHom.op
added def MonoidHom.unop
added def MulEquiv.inv'
added def MulEquiv.op
added def MulEquiv.unop
added def MulHom.op
added def MulHom.unop
added theorem MulOpposite.commute_op
added theorem MulOpposite.op_div
added theorem MulOpposite.unop_div
added theorem SemiconjBy.op
added theorem SemiconjBy.unop
added def Units.opEquiv