Theorem MulMemClass.coe_subtype

Modification history

2024-10-28 17:42

Mathlib/Algebra/Group/Subsemigroup/Defs.lean

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

Modified MulMemClass.coe_subtype View on Github →

2022-12-31 09:21

Mathlib/GroupTheory/Subsemigroup/Operations.lean

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

Added MulMemClass.coe_subtype View on Github →