Theorem MulEquiv.isSimpleGroup_congr

Modification history

2025-07-15 08:10
Mathlib/GroupTheory/Subgroup/Simple.lean
feat: equivalent condition for subgroups to be simple (#26552) …
Added MulEquiv.isSimpleGroup_congrView on Github →