Commit 2024-12-20 09:05 31a16b3f
View on Github →feat(GroupTheory/Solvable): Prove isSolvable_iff_commutator_lt (#20107)
A finite group is solvable if and only if [H, H] < H for all nontrivial subgroups H.
feat(GroupTheory/Solvable): Prove isSolvable_iff_commutator_lt (#20107)
A finite group is solvable if and only if [H, H] < H for all nontrivial subgroups H.