Commit 2025-05-10 20:57 5495f46c

View on Github →

chore: move AddMonoidHom.mul out of Algebra.Group (#24701) It's about rings!

Estimated changes

deleted theorem AddMonoidHom.coe_flip_mul
deleted theorem AddMonoidHom.coe_mul
deleted theorem AddMonoidHom.map_mul_iff
deleted def AddMonoidHom.mul
deleted theorem AddMonoidHom.mul_apply
added theorem AddMonoidHom.coe_mul
modified theorem AddMonoidHom.coe_mulLeft
modified theorem AddMonoidHom.coe_mulRight
added def AddMonoidHom.mul
modified def AddMonoidHom.mulLeft
modified def AddMonoidHom.mulRight
modified theorem AddMonoidHom.mulRight_apply
added theorem AddMonoidHom.mul_apply