Commit 2026-04-29 17:24 2af034a3

View on Github →

chore(GroupTheory/Nilpotent): move declarations into namespace (#37175) This PR moves the declarations of GroupTheory/Nilpotent from the root namespace to either the Subgroup namespace or the Group namespace. I also switched over to the commutator element notation in a few places.

Estimated changes

Modified Mathlib/GroupTheory/Commutator/Basic.lean

Modified Mathlib/GroupTheory/Frattini.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

added theorem Group.isNilpotent_of_finite_tfae

added theorem Group.isNilpotent_of_product_of_sylow_group

added theorem Group.isNilpotent_pi_of_bounded_class

added theorem Group.nilpotencyClass_eq_quotient_center_plus_one

added theorem Group.nilpotencyClass_le_of_ker_le_center

added theorem Group.nilpotencyClass_le_of_surjective

added theorem Group.nilpotencyClass_le_one_of_isSimple_of_isNilpotent

added theorem Group.nilpotencyClass_pi

added theorem Group.nilpotencyClass_prod

added theorem Group.nilpotencyClass_quotient_center

added theorem Group.nilpotencyClass_quotient_le

added theorem Group.nilpotencyClass_zero_iff_subsingleton

added theorem Group.nilpotent_center_quotient_ind

added theorem Group.nilpotent_of_mulEquiv

added theorem Group.nilpotent_of_surjective

added theorem Group.normalizerCondition_of_isNilpotent

added theorem Group.of_quotient_center_nilpotent

deleted def IsAscendingCentralSeries

deleted def IsDescendingCentralSeries

added def Subgroup.IsAscendingCentralSeries

added def Subgroup.IsDescendingCentralSeries

added theorem Subgroup.ascending_central_series_le_upper

added theorem Subgroup.comap_upperCentralSeries

added theorem Subgroup.comap_upperCentralSeries_quotient_center

added theorem Subgroup.derived_le_lower_central

added theorem Subgroup.descending_central_series_ge_lower

added theorem Subgroup.isNilpotent_of_ker_le_center

added theorem Subgroup.is_ascending_rev_series_of_is_descending

added theorem Subgroup.is_descending_rev_series_of_is_ascending

added theorem Subgroup.least_ascending_central_series_length_eq_nilpotencyClass

added theorem Subgroup.least_descending_central_series_length_eq_nilpotencyClass

added theorem Subgroup.lowerCentralSeries.map

added def Subgroup.lowerCentralSeries

added theorem Subgroup.lowerCentralSeries_antitone

added theorem Subgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le

added theorem Subgroup.lowerCentralSeries_isDescendingCentralSeries

added theorem Subgroup.lowerCentralSeries_length_eq_nilpotencyClass

added theorem Subgroup.lowerCentralSeries_map_subtype_le

added theorem Subgroup.lowerCentralSeries_nilpotencyClass

added theorem Subgroup.lowerCentralSeries_one

added theorem Subgroup.lowerCentralSeries_pi_le

added theorem Subgroup.lowerCentralSeries_pi_of_finite

added theorem Subgroup.lowerCentralSeries_prod

added theorem Subgroup.lowerCentralSeries_succ

added theorem Subgroup.lowerCentralSeries_succ_eq_bot

added theorem Subgroup.lowerCentralSeries_zero

added theorem Subgroup.mem_lowerCentralSeries_succ_iff

added theorem Subgroup.mem_upperCentralSeriesStep

added theorem Subgroup.mem_upperCentralSeries_succ_iff

modified theorem Subgroup.nilpotencyClass_le

added theorem Subgroup.nilpotencyClass_le_of_upperCentralSeries_eq

added theorem Subgroup.nilpotent_iff_finite_ascending_central_series

added theorem Subgroup.nilpotent_iff_finite_descending_central_series

added theorem Subgroup.nilpotent_iff_lowerCentralSeries

added theorem Subgroup.upperCentralSeries.StrictMonoOn

added theorem Subgroup.upperCentralSeries.card_image_eq_of_le_nilpotencyClass

added theorem Subgroup.upperCentralSeries.eq_ge_of_eq_gt

added theorem Subgroup.upperCentralSeries.eq_ge_of_eq_succ

added theorem Subgroup.upperCentralSeries.eq_top

added theorem Subgroup.upperCentralSeries.map

added def Subgroup.upperCentralSeries

added def Subgroup.upperCentralSeriesAux

added def Subgroup.upperCentralSeriesStep

added theorem Subgroup.upperCentralSeriesStep_eq_comap_center

added theorem Subgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le

added theorem Subgroup.upperCentralSeries_isAscendingCentralSeries

added theorem Subgroup.upperCentralSeries_mono

added theorem Subgroup.upperCentralSeries_nilpotencyClass

added theorem Subgroup.upperCentralSeries_one

added theorem Subgroup.upperCentralSeries_zero

deleted theorem ascending_central_series_le_upper

deleted theorem comap_upperCentralSeries

deleted theorem comap_upperCentralSeries_quotient_center

deleted theorem derived_le_lower_central

deleted theorem descending_central_series_ge_lower

deleted theorem isNilpotent_of_finite_tfae

deleted theorem isNilpotent_of_ker_le_center

deleted theorem isNilpotent_of_product_of_sylow_group

deleted theorem isNilpotent_pi_of_bounded_class

deleted theorem is_ascending_rev_series_of_is_descending

deleted theorem is_descending_rev_series_of_is_ascending

deleted theorem least_ascending_central_series_length_eq_nilpotencyClass

deleted theorem least_descending_central_series_length_eq_nilpotencyClass

deleted theorem lowerCentralSeries.map

deleted def lowerCentralSeries

deleted theorem lowerCentralSeries_antitone

deleted theorem lowerCentralSeries_eq_bot_iff_nilpotencyClass_le

deleted theorem lowerCentralSeries_isDescendingCentralSeries

deleted theorem lowerCentralSeries_length_eq_nilpotencyClass

deleted theorem lowerCentralSeries_map_subtype_le

deleted theorem lowerCentralSeries_nilpotencyClass

deleted theorem lowerCentralSeries_one

deleted theorem lowerCentralSeries_pi_le

deleted theorem lowerCentralSeries_pi_of_finite

deleted theorem lowerCentralSeries_prod

deleted theorem lowerCentralSeries_succ

deleted theorem lowerCentralSeries_succ_eq_bot

deleted theorem lowerCentralSeries_zero

deleted theorem mem_lowerCentralSeries_succ_iff

deleted theorem mem_upperCentralSeriesStep

deleted theorem mem_upperCentralSeries_succ_iff

deleted theorem nilpotencyClass_eq_quotient_center_plus_one

deleted theorem nilpotencyClass_le_of_ker_le_center

deleted theorem nilpotencyClass_le_of_surjective

deleted theorem nilpotencyClass_le_of_upperCentralSeries_eq

deleted theorem nilpotencyClass_le_one_of_isSimple_of_isNilpotent

deleted theorem nilpotencyClass_pi

deleted theorem nilpotencyClass_prod

deleted theorem nilpotencyClass_quotient_center

deleted theorem nilpotencyClass_quotient_le

deleted theorem nilpotencyClass_zero_iff_subsingleton

deleted theorem nilpotent_center_quotient_ind

deleted theorem nilpotent_iff_finite_ascending_central_series

deleted theorem nilpotent_iff_finite_descending_central_series

deleted theorem nilpotent_iff_lowerCentralSeries

deleted theorem nilpotent_of_mulEquiv

deleted theorem nilpotent_of_surjective

deleted theorem normalizerCondition_of_isNilpotent

deleted theorem of_quotient_center_nilpotent

deleted theorem upperCentralSeries.StrictMonoOn

deleted theorem upperCentralSeries.card_image_eq_of_le_nilpotencyClass

deleted theorem upperCentralSeries.eq_ge_of_eq_gt

deleted theorem upperCentralSeries.eq_ge_of_eq_succ

deleted theorem upperCentralSeries.eq_top

deleted theorem upperCentralSeries.map

deleted def upperCentralSeries

deleted def upperCentralSeriesAux

deleted def upperCentralSeriesStep

deleted theorem upperCentralSeriesStep_eq_comap_center

deleted theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le

deleted theorem upperCentralSeries_isAscendingCentralSeries

deleted theorem upperCentralSeries_mono

deleted theorem upperCentralSeries_nilpotencyClass

deleted theorem upperCentralSeries_one

deleted theorem upperCentralSeries_zero

Modified Mathlib/GroupTheory/SpecificGroups/ZGroup.lean