Commit 2025-07-23 15:29 ef9f2260

View on Github →

chore(GroupTheory/FreeAbelianGroup): do not import cardinals (#27169) Move the Fintype and Cardinal material from GroupTheory.Coset.Basic to GroupTheory.Coset.Card. That was just misplaced. Split GroupTheory.Abelianization into:

  • more material in GroupTheory.Commutator.Basic and GroupTheory.Commutator.Finite that was just misplaced
  • GroupTheory.Abelianization.Defs for the definition of the abelianisation
  • GroupTheory.Abelianization.Finite for the finiteness of the abelianisation of a finite group

Estimated changes

deleted theorem Abelianization.hom_ext
deleted theorem Abelianization.ker_of
deleted theorem Abelianization.lift.of
deleted def Abelianization.lift
deleted theorem Abelianization.lift_of
deleted def Abelianization.map
deleted theorem Abelianization.map_comp
deleted theorem Abelianization.map_id
deleted theorem Abelianization.map_of
deleted theorem Abelianization.mk_eq_of
deleted def Abelianization.of
deleted def Abelianization
deleted theorem abelianizationCongr_of
deleted theorem abelianizationCongr_refl
deleted theorem abelianizationCongr_symm
deleted theorem abelianizationCongr_trans
deleted def commutator
deleted theorem commutator_def
deleted theorem commutator_eq_closure
deleted theorem map_commutator_eq
deleted theorem rank_commutator_le_card
added theorem Abelianization.hom_ext
added theorem Abelianization.ker_of
added theorem Abelianization.lift.of
added theorem Abelianization.lift_of
added theorem Abelianization.map_id
added theorem Abelianization.map_of
added def Abelianization
added theorem abelianizationCongr_of
added def commutator
added theorem commutator_def
added theorem commutator_eq_closure
added theorem map_commutator_eq