Commit 2026-08-17 05:33 4e0ca9d9

View on Github →

feat(IsMulCommutative): generalize lemma from MulHom to MulHomClass (#42635)

Estimated changes

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

added theorem Function.Surjective.isMulCommutative

deleted theorem Function.Surjective.mul_comm

Modified Mathlib/GroupTheory/Commutator/Basic.lean