Commit 2023-03-06 05:02 5c44c6f8

View on Github →

feat: port GroupTheory.Solvable (#2221)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Solvable.lean

added theorem Equiv.Perm.fin_5_not_solvable

added theorem Equiv.Perm.not_solvable

added theorem IsSimpleGroup.comm_iff_isSolvable

added theorem IsSimpleGroup.derivedSeries_succ

added def derivedSeries

added theorem derivedSeries_le_map_derivedSeries

added theorem derivedSeries_normal

added theorem derivedSeries_one

added theorem derivedSeries_succ

added theorem derivedSeries_zero

added theorem isSolvable_def

added theorem isSolvable_of_comm

added theorem isSolvable_of_top_eq_bot

added theorem map_derivedSeries_eq

added theorem map_derivedSeries_le_derivedSeries

added theorem not_solvable_of_mem_derivedSeries

added theorem solvable_of_ker_le_range

added theorem solvable_of_solvable_injective

added theorem solvable_of_surjective