Commit 2026-02-16 08:27 d0486529

feat(GroupTheory): each term in a upper(lower) central series is a characteristic subgroup (#34890) The main lemma proved in this PR is Subgroup.Characteristic.quotient, which says that if H is a characteristic subgroup of G, and K is a characteristic subgroup of G / H, then the preimage of K under the projection map is a characteristic subgroup of G. As a corollary, I proved that each term in the upper central series is a characteristic subgroup. I deleted the instances related to normality as normality can be inferred from being characteristic.