Commit 2023-05-31 06:20 40237d16

View on Github →

feat: port GroupTheory.Nilpotent (#4472)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Nilpotent.lean

added theorem CommGroup.nilpotencyClass_le_one

added theorem Group.IsNilpotent.nilpotent

added def IsAscendingCentralSeries

added def IsDescendingCentralSeries

added theorem IsPGroup.isNilpotent

added theorem Subgroup.nilpotencyClass_le

added theorem ascending_central_series_le_upper

added theorem comap_upperCentralSeries_quotient_center

added def commGroupOfNilpotencyClass

added theorem derived_le_lower_central

added theorem descending_central_series_ge_lower

added theorem isNilpotent_of_finite_tFAE

added theorem isNilpotent_of_ker_le_center

added theorem isNilpotent_of_product_of_sylow_group

added theorem isNilpotent_pi_of_bounded_class

added theorem is_ascending_rev_series_of_is_descending

added theorem is_decending_rev_series_of_is_ascending

added theorem least_ascending_central_series_length_eq_nilpotencyClass

added theorem least_descending_central_series_length_eq_nilpotencyClass

added theorem lowerCentralSeries.map

added def lowerCentralSeries

added theorem lowerCentralSeries_antitone

added theorem lowerCentralSeries_eq_bot_iff_nilpotencyClass_le

added theorem lowerCentralSeries_isDescendingCentralSeries

added theorem lowerCentralSeries_length_eq_nilpotencyClass

added theorem lowerCentralSeries_map_subtype_le

added theorem lowerCentralSeries_nilpotencyClass

added theorem lowerCentralSeries_one

added theorem lowerCentralSeries_pi_le

added theorem lowerCentralSeries_pi_of_finite

added theorem lowerCentralSeries_prod

added theorem lowerCentralSeries_succ

added theorem lowerCentralSeries_succ_eq_bot

added theorem lowerCentralSeries_zero

added theorem mem_lowerCentralSeries_succ_iff

added theorem mem_upperCentralSeriesStep

added theorem mem_upperCentralSeries_succ_iff

added theorem nilpotencyClass_eq_quotient_center_plus_one

added theorem nilpotencyClass_le_of_ker_le_center

added theorem nilpotencyClass_le_of_surjective

added theorem nilpotencyClass_pi

added theorem nilpotencyClass_prod

added theorem nilpotencyClass_quotient_center

added theorem nilpotencyClass_quotient_le

added theorem nilpotencyClass_zero_iff_subsingleton

added theorem nilpotent_center_quotient_ind

added theorem nilpotent_iff_finite_ascending_central_series

added theorem nilpotent_iff_finite_descending_central_series

added theorem nilpotent_iff_lowerCentralSeries

added theorem nilpotent_of_mulEquiv

added theorem nilpotent_of_surjective

added theorem normalizerCondition_of_isNilpotent

added theorem of_quotient_center_nilpotent

added theorem upperCentralSeries.map

added def upperCentralSeries

added def upperCentralSeriesAux

added def upperCentralSeriesStep

added theorem upperCentralSeriesStep_eq_comap_center

added theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le

added theorem upperCentralSeries_isAscendingCentralSeries

added theorem upperCentralSeries_mono

added theorem upperCentralSeries_nilpotencyClass

added theorem upperCentralSeries_one

added theorem upperCentralSeries_zero