Commit 2021-08-23 16:02 9a7d9a8e

View on Github →

feat(group_theory/nilpotent): add def lemmas, basic lemmas on central series (#8730) Add to API for nilpotent groups with simp def lemmas and other basic properties of central series.

Estimated changes

Modified src/group_theory/nilpotent.lean

modified def is_ascending_central_series

added theorem lower_central_series_zero

added theorem mem_lower_central_series_succ_iff

modified theorem mem_upper_central_series_succ_iff

added theorem upper_central_series.map

added theorem upper_central_series_mono

added theorem upper_central_series_zero

deleted theorem upper_central_series_zero_def