Commit 2023-01-27 13:00 bf59cf69

View on Github →

feat: port GroupTheory.Subgroup.Simple (#1858)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Subgroup/Simple.lean

added theorem IsSimpleGroup.isSimpleGroup_of_surjective

added theorem Subgroup.Normal.eq_bot_or_eq_top