Theorem Function.Surjective.isMulCommutative

Modification history

2026-08-17 05:33
Mathlib/Algebra/Group/Hom/Defs.lean
feat(IsMulCommutative): generalize lemma from MulHom to MulHomClass (#42635)
Added Function.Surjective.isMulCommutativeView on Github →