Commit 2025-04-24 08:21 44efe040

View on Github →

chore(GroupTheory/Finiteness): move Group.rank to a new file (#24326) That reduces imports by quite a lot: We don't even import MonoidWithZero anymore! See https://github.com/leanprover-community/mathlib3/pull/12765 for the new copyright header. From Toric

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Abelianization.lean

Modified Mathlib/GroupTheory/Commutator/Finite.lean

Modified Mathlib/GroupTheory/Finiteness.lean

deleted theorem Group.rank_congr

deleted theorem Group.rank_le

deleted theorem Group.rank_le_of_surjective

deleted theorem Group.rank_range_le

deleted theorem Group.rank_spec

deleted theorem Subgroup.nat_card_centralizer_nat_card_stabilizer

deleted theorem Subgroup.rank_closure_finite_le_nat_card

deleted theorem Subgroup.rank_closure_finset_le_card

deleted theorem Subgroup.rank_congr

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Created Mathlib/GroupTheory/Rank.lean

added theorem Group.rank_congr

added theorem Group.rank_le

added theorem Group.rank_le_of_surjective

added theorem Group.rank_range_le

added theorem Group.rank_spec

added theorem Subgroup.nat_card_centralizer_nat_card_stabilizer

added theorem Subgroup.rank_closure_finite_le_nat_card

added theorem Subgroup.rank_closure_finset_le_card

added theorem Subgroup.rank_congr

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/NumberTheory/PellMatiyasevic.lean