mathlib

87bc893a - feat(group_theory/{subgroup, order_of_element}): refactors simple groups, classifies finite simple abelian/solvable groups (#6926)

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_group`s are cyclic Shows that all simple finite `comm_group`s have prime order Shows that a simple group is solvable iff it is commutative