Theorem isMulCommutative_iff

Modification history

2026-08-20 19:44

Mathlib/Algebra/Group/Defs.lean

refactor(Algebra/Group): split overlong file Defs.lean (#42952) …

Modified isMulCommutative_iff View on Github →

2026-04-09 03:01

Mathlib/Algebra/Group/Defs.lean

chore(Algebra): use `IsMulCommutative` to spell `Std.Commutative (· * ·)` (#37448) …

Modified isMulCommutative_iff View on Github →

2026-03-31 10:44

Mathlib/Algebra/Group/Defs.lean

refactor: use `IsMulCommutative` ubiquitously for subobjects (#36549) …

Added isMulCommutative_iff View on Github →