Commit 2023-02-11 21:40 b10c1d7a

View on Github →

feat: port GroupTheory.Abelianization (#2215)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Abelianization.lean

added theorem Abelianization.commutator_subset_ker

added def Abelianization.equivOfComm

added theorem Abelianization.hom_ext

added theorem Abelianization.lift.of

added theorem Abelianization.lift.unique

added def Abelianization.lift

added theorem Abelianization.lift_of

added def Abelianization.map

added theorem Abelianization.map_comp

added theorem Abelianization.map_id

added theorem Abelianization.map_map_apply

added theorem Abelianization.map_of

added theorem Abelianization.mk_eq_of

added def Abelianization.of

added def Abelianization

added def MulEquiv.abelianizationCongr

added theorem abelianizationCongr_of

added theorem abelianizationCongr_refl

added theorem abelianizationCongr_symm

added theorem abelianizationCongr_trans

added theorem card_commutatorSet_closureCommutatorRepresentatives

added theorem card_commutator_closureCommutatorRepresentatives

added def closureCommutatorRepresentatives

added def commutator

added def commutatorRepresentatives

added theorem commutator_centralizer_commutator_le_center

added theorem commutator_def

added theorem commutator_eq_closure

added theorem commutator_eq_normalClosure

added theorem image_commutatorSet_closureCommutatorRepresentatives

added theorem rank_closure_commutator_representations_le

added theorem rank_commutator_le_card