Commit 2025-04-09 17:03 e54e0c69
View on Github →chore(Algebra/Group/Ext): use hMul rather than mul for group extensionality (#23875) Each of the other extensionality principles use hMul rather than mul in this way, as described and explained in the module docstring. However, Group and CommGroup were omitted from this pattern, which is corrected here.