Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nilpotent_of_mul_equiv

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 nilpotent_of_mul_equivView on Github →