Theorem isMulCommutative_anti

Modification history

2026-08-25 11:58

Mathlib/Algebra/Group/Subsemigroup/Defs.lean

feat: `isMulCommutative_anti` for subobjects (#43024)

Added isMulCommutative_anti View on Github →