Theorem Subgroup.mul_comm_of_mem_isCommutative

Modification history

2025-04-10 07:25
Mathlib/Algebra/Group/Subgroup/Defs.lean
chore(GroupTheory): Add the class `IsMulCommutative` (#23773) …
Deleted Subgroup.mul_comm_of_mem_isCommutativeView on Github →
2024-10-28 17:42
Mathlib/Algebra/Group/Subgroup/Basic.lean
chore(Algebra/Group/Subgroup): split off `Defs` file (#18340) …
Modified Subgroup.mul_comm_of_mem_isCommutativeView on Github →
2024-08-07 11:50
Mathlib/Algebra/Group/Subgroup/Basic.lean
feat(Subgroup/IsCommutative): add instance for MonoidHom.range (#15370) …
Added Subgroup.mul_comm_of_mem_isCommutativeView on Github →