Commit 2025-11-07 12:32 b52ea70e

View on Github →

feat: MonoidHom.toAdditiveRight as a MulEquiv (#27047) From Toric

Estimated changes

Modified Mathlib/Algebra/Group/TypeTags/Hom.lean

added def AddMonoidHom.toMultiplicativeLeftAddEquiv

added def AddMonoidHom.toMultiplicativeRightAddEquiv

added theorem AddMonoidHom.toMultiplicative_add

added theorem AddMonoidHom.toMultiplicative_id

added theorem MonoidHom.coe_toAdditive

deleted theorem MonoidHom.coe_toMultiplicative

added def MonoidHom.toAdditiveLeftMulEquiv

added def MonoidHom.toAdditiveRightMulEquiv

added theorem MonoidHom.toAdditive_id