Commit 2026-08-25 11:58 a88b3f9e

View on Github →

feat: isMulCommutative_anti for subobjects (#43024)

Estimated changes

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

added theorem isMulCommutative_anti

modified theorem isMulCommutative_iff_of_setLike

modified theorem setLike_mul_comm