Theorem IsSolvable.commutator_lt_of_ne_bot

Modification history

2024-12-20 09:05
Mathlib/GroupTheory/Solvable.lean
feat(GroupTheory/Solvable): Prove `isSolvable_iff_commutator_lt` (#20107) …
Added IsSolvable.commutator_lt_of_ne_botView on Github →