Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_p_group.is_nilpotent

Modification history

2022-08-17 14:53
src/group_theory/nilpotent.lean
chore(group_theory/*): Fix lint (#16095) …
Modified is_p_group.is_nilpotentView on Github →
2022-02-27 01:14
src/group_theory/nilpotent.lean
feat(group_theory/nilpotent): is_nilpotent_of_product_of_sylow_group (#11834)
Modified is_p_group.is_nilpotentView on Github →
2022-02-02 10:56
src/group_theory/nilpotent.lean
feat(group_theory/nilpotent): p-groups are nilpotent (#11726)
Added is_p_group.is_nilpotentView on Github →