Theorem MulMemClass.mul_def

Modification history

2024-10-28 17:42

Mathlib/Algebra/Group/Subsemigroup/Defs.lean

chore(Algebra/Group/Subgroup): split off `Defs` file (#18340) …

Modified MulMemClass.mul_def View on Github →

2022-12-31 09:21

Mathlib/GroupTheory/Subsemigroup/Operations.lean

feat: port GroupTheory.Subsemigroup.Operations (#1235)

Added MulMemClass.mul_def View on Github →