Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-21 11:37 d8d2f543

View on Github →

feat(group_theory/nilpotent): n-ary products of nilpotent group (#11829)

Estimated changes

Modified src/group_theory/nilpotent.lean

added theorem is_nilpotent_pi_of_bounded_class

added theorem lower_central_series_pi_le

added theorem lower_central_series_pi_of_fintype

added theorem nilpotency_class_pi