Theorem IsSolvable.commutator_lt_of_ne_bot

Modification history

2026-07-17 16:51

Mathlib/GroupTheory/Solvable.lean

chore(GroupTheory): rename `IsSolvable` to `Group.IsSolvable` (#41820) …

Deleted IsSolvable.commutator_lt_of_ne_bot View on Github →

2024-12-20 09:05

Mathlib/GroupTheory/Solvable.lean

feat(GroupTheory/Solvable): Prove `isSolvable_iff_commutator_lt` (#20107) …

Added IsSolvable.commutator_lt_of_ne_bot View on Github →