nilpotent): solvable_of_nilpotent (#11512)

Commit

3 years ago

feat(src/group_theory/nilpotent): solvable_of_nilpotent (#11512) following the proof on <https://groupprops.subwiki.org/wiki/Nilpotent_implies_solvable>

Author

nomeata

Parents

274b5309

mathlib3 40725122 - feat(src/group_theory/nilpotent): solvable_of_nilpotent (#11512)

mathlib3
40725122 - feat(src/group_theory/nilpotent): solvable_of_nilpotent (#11512)