Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-29 23:43 87bc893a

View on Github →

feat(group_theory/{subgroup, order_of_element}): refactors simple groups, classifies finite simple abelian/solvable groups (#6926) Refactors the deprecated simple_group to a new is_simple_group Shows that all cyclic groups of prime order are simple Shows that all simple comm_groups are cyclic Shows that all simple finite comm_groups have prime order Shows that a simple group is solvable iff it is commutative

Estimated changes