Commit 2021-08-16 16:19 106bd3be

View on Github →

feat(group_theory/nilpotent): add nilpotent groups (#8538) We make basic definitions of nilpotent groups and prove the standard theorem that a group is nilpotent iff the upper resp. lower central series reaches top resp. bot.

Estimated changes

Modified src/group_theory/coset.lean

added theorem quotient_group.forall_coe

Created src/group_theory/nilpotent.lean

added theorem ascending_central_series_le_upper

added theorem descending_central_series_ge_lower

added def is_ascending_central_series

added def is_descending_central_series

added def lower_central_series

added theorem lower_central_series_is_descending_central_series

added theorem mem_upper_central_series_step

added theorem mem_upper_central_series_succ_iff

added theorem nilpotent_iff_finite_ascending_central_series

added theorem nilpotent_iff_finite_descending_central_series

added theorem nilpotent_iff_lower_central_series

added def upper_central_series

added def upper_central_series_aux

added theorem upper_central_series_is_ascending_central_series

added def upper_central_series_step

added theorem upper_central_series_step_eq_comap_center

added theorem upper_central_series_zero_def