Theorem IsSolvable.commutator_lt_top_of_nontrivial

Modification history

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