Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-06 08:30 5f98a961

View on Github →

feat(group_theory): add definition of solvable group (#5565) Defines solvable groups using the definition that a group is solvable if its nth commutator is eventually trivial. Defines the nth commutator of a group and provides some lemmas for working with it. More facts about solvable groups will come in future PRs.

Estimated changes