Theorem Subgroup.Normal.eq_bot_or_eq_top

Modification history

2026-09-16 10:29
Mathlib/GroupTheory/Subgroup/Simple.lean
refactor(GroupTheory/Subgroup/Simple): make normality an instance argument in `IsSimpleGroup` (#43864) …
Modified Subgroup.Normal.eq_bot_or_eq_topView on Github →
2023-01-27 13:00
Mathlib/GroupTheory/Subgroup/Simple.lean
feat: port GroupTheory.Subgroup.Simple (#1858)
Added Subgroup.Normal.eq_bot_or_eq_topView on Github →