Commit 2026-05-28 16:48 8d6d03d8

feat(GroupTheory): subgroup-valued lower central series (#39844) This PR replaces Subgroup.lowerCentralSeries (G : Type*) with the more general Subgroup.lowerCentralSeries (S : Subgroup G), the iterated commutator ⁅⁅⋯⁅S, S⁆, S⁆⋯, S⁆ of S with itself viewed in the ambient group G. The classical lower central series of G becomes the case S = ⊤; most of the existing API (_zero, _succ, _antitone, _le_self, _mono, map_*, the prod and pi versions) generalizes to arbitrary subgroups, and the proofs of Subgroup.isNilpotent and Subgroup.nilpotencyClass_le shed the .map S.subtype plumbing. Motivation: requested on #mathlib4 > Subgroup.lowerCentralSeries; needed to clean up the Fitting's theorem PR (#39813). 🤖 Prepared with Claude Code