Theorem Subgroup.smul_opposite_mul

Modification history

2023-09-28 12:57

Mathlib/GroupTheory/Subgroup/MulOpposite.lean

feat(GroupTheory/Submonoid): add opposite submonoids (#7415) …

Modified Subgroup.smul_opposite_mul View on Github →

2023-01-26 16:39

Mathlib/GroupTheory/Subgroup/MulOpposite.lean

feat: port GroupTheory.Subgroup.MulOpposite (#1857) …

Added Subgroup.smul_opposite_mul View on Github →