Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_nilpotent_of_product_of_sylow_group

Modification history

2022-02-27 01:14
src/group_theory/nilpotent.lean
feat(group_theory/nilpotent): is_nilpotent_of_product_of_sylow_group (#11834)
Added is_nilpotent_of_product_of_sylow_groupView on Github →