Commit 2025-03-03 14:53 aceeedb3

View on Github →

chore: make MulOpposite more primitive (#22395) This way, we can ensure that the instances for left and right multiplications stay together rather than the right ones being dumped in faraway files. See https://github.com/leanprover-community/mathlib3/pull/2339 for the new copyright header.

Estimated changes

added def AddEquiv.mulOp
added def AddEquiv.mulUnop
added def AddHom.mulOp
added def AddHom.mulUnop
added def MonoidHom.op
added def MonoidHom.unop
added def MulEquiv.inv'
added def MulEquiv.op
added def MulEquiv.opOp
added def MulEquiv.unop
added def MulHom.op
added def MulHom.unop
deleted def AddEquiv.mulOp
deleted def AddEquiv.mulUnop
deleted def AddHom.mulOp
deleted def AddHom.mulUnop
deleted def AddMonoidHom.mulOp
deleted theorem AddMonoidHom.mul_op_ext
deleted def MonoidHom.op
deleted def MonoidHom.unop
deleted def MulEquiv.inv'
deleted def MulEquiv.op
deleted def MulEquiv.opOp
deleted def MulEquiv.unop
deleted def MulHom.fromOpposite
deleted def MulHom.op
deleted def MulHom.toOpposite
deleted def MulHom.unop