Commit 2026-06-24 00:45 62dc8f26

View on Github →

feat(GroupTheory/IsPerfect): Grün's lemma (#39956) Grün's lemma: In a perfect group (commutator G = ⊤), center (G ⧸ center G) = ⊥. Also the derivedSeries and the lowerCentralSeries are a constant ⊤, and the upperCentralSeries starts with ⊥ and afterwards is a constant center G.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Ker.lean

added theorem MonoidHom.comap_range_self

added theorem MonoidHom.ker_le_comap

added theorem Subgroup.comap_eq_ker

added theorem Subgroup.comap_eq_ker_of_surjective

added theorem Subgroup.map_ker_self

Modified Mathlib/GroupTheory/Commutator/Basic.lean

added theorem Subgroup.commutator_center_left

added theorem Subgroup.commutator_center_right

added theorem Subgroup.commutator_self_eq_bot_iff

added theorem Subgroup.commutator_top_left_eq_bot_iff_le_center

added theorem Subgroup.commutator_top_right_eq_bot_iff_le_center

Modified Mathlib/GroupTheory/IsPerfect.lean

added theorem Group.IsPerfect.center_quotient_center_eq_bot

added theorem Group.IsPerfect.derivedSeries_eq_top

added theorem Group.IsPerfect.lowerCentralSeries_eq_top

added theorem Group.IsPerfect.upperCentralSeries_eq_center

Modified Mathlib/GroupTheory/Nilpotent.lean

added theorem Subgroup.commutator_upperCentralSeries_top_le

Modified Mathlib/GroupTheory/Subgroup/Centralizer.lean

added theorem Subgroup.centralizer_center