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 leanprover-community/mathlib3#12765 for the new copyright header.

From Toric

Author: YaelDillies

Mathlib.lean

@@ -3693,6 +3693,7 @@ import Mathlib.GroupTheory.PushoutI
 import Mathlib.GroupTheory.QuotientGroup.Basic
 import Mathlib.GroupTheory.QuotientGroup.Defs
 import Mathlib.GroupTheory.QuotientGroup.Finite
+import Mathlib.GroupTheory.Rank
 import Mathlib.GroupTheory.Schreier
 import Mathlib.GroupTheory.SchurZassenhaus
 import Mathlib.GroupTheory.SemidirectProduct

Mathlib/GroupTheory/Abelianization.lean

@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Michael Howes, Antoine Chambert-Loir
 -/
 import Mathlib.Data.Finite.Card
-import Mathlib.Data.Finite.Prod
 import Mathlib.GroupTheory.Commutator.Basic
 import Mathlib.GroupTheory.Coset.Basic
-import Mathlib.GroupTheory.Finiteness
+import Mathlib.GroupTheory.Rank
 
 /-!
 # The abelianization of a group

Mathlib/GroupTheory/Commutator/Finite.lean

@@ -5,7 +5,7 @@ Authors: Jordan Brown, Thomas Browning, Patrick Lutz
 -/
 import Mathlib.Algebra.Group.Subgroup.Finite
 import Mathlib.GroupTheory.Commutator.Basic
-import Mathlib.GroupTheory.Finiteness
+import Mathlib.GroupTheory.Rank
 import Mathlib.GroupTheory.Index
 
 /-!

Mathlib/GroupTheory/Finiteness.lean

@@ -6,7 +6,6 @@ Authors: Riccardo Brasca
 import Mathlib.Algebra.Group.Pointwise.Set.Finite
 import Mathlib.Algebra.Group.Subgroup.Pointwise
 import Mathlib.GroupTheory.QuotientGroup.Defs
-import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
 # Finitely generated monoids and groups
@@ -25,6 +24,7 @@ group.
 
 -/
 
+assert_not_exists MonoidWithZero
 
 /-! ### Monoids and submonoids -/
 
@@ -317,80 +317,8 @@ instance Group.closure_finite_fg (s : Set G) [Finite s] : Group.FG (Subgroup.clo
   haveI := Fintype.ofFinite s
   s.coe_toFinset ▸ Group.closure_finset_fg s.toFinset
 
-variable (G)
-
-/-- The minimum number of generators of a group. -/
-@[to_additive "The minimum number of generators of an additive group"]
-noncomputable def Group.rank [h : Group.FG G] :=
-  @Nat.find _ (Classical.decPred _) (Group.fg_iff'.mp h)
-
-@[to_additive]
-theorem Group.rank_spec [h : Group.FG G] :
-    ∃ S : Finset G, S.card = Group.rank G ∧ Subgroup.closure (S : Set G) = ⊤ :=
-  @Nat.find_spec _ (Classical.decPred _) (Group.fg_iff'.mp h)
-
-@[to_additive]
-theorem Group.rank_le [h : Group.FG G] {S : Finset G} (hS : Subgroup.closure (S : Set G) = ⊤) :
-    Group.rank G ≤ S.card :=
-  @Nat.find_le _ _ (Classical.decPred _) (Group.fg_iff'.mp h) ⟨S, rfl, hS⟩
-
-variable {G} {G' : Type*} [Group G']
-
-@[to_additive]
-theorem Group.rank_le_of_surjective [Group.FG G] [Group.FG G'] (f : G →* G')
-    (hf : Function.Surjective f) : Group.rank G' ≤ Group.rank G := by
-  classical
-    obtain ⟨S, hS1, hS2⟩ := Group.rank_spec G
-    trans (S.image f).card
-    · apply Group.rank_le
-      rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
-    · exact Finset.card_image_le.trans_eq hS1
-
-@[to_additive]
-theorem Group.rank_range_le [Group.FG G] {f : G →* G'} : Group.rank f.range ≤ Group.rank G :=
-  Group.rank_le_of_surjective f.rangeRestrict f.rangeRestrict_surjective
-
-@[to_additive]
-theorem Group.rank_congr [Group.FG G] [Group.FG G'] (f : G ≃* G') : Group.rank G = Group.rank G' :=
-  le_antisymm (Group.rank_le_of_surjective f.symm f.symm.surjective)
-    (Group.rank_le_of_surjective f f.surjective)
-
 end Group
 
-namespace Subgroup
-
-@[to_additive]
-theorem rank_congr {H K : Subgroup G} [Group.FG H] [Group.FG K] (h : H = K) :
-    Group.rank H = Group.rank K := by subst h; rfl
-
-@[to_additive]
-theorem rank_closure_finset_le_card (s : Finset G) : Group.rank (closure (s : Set G)) ≤ s.card := by
-  classical
-  let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
-  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
-    rw [Finset.coe_preimage]
-    exact closure_preimage_eq_top (s : Set G)
-  apply (Group.rank_le (closure (s : Set G)) ht).trans
-  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
-    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
-    apply Finset.card_filter_le
-  apply Subtype.coe_injective.injOn
-
-@[to_additive]
-theorem rank_closure_finite_le_nat_card (s : Set G) [Finite s] :
-    Group.rank (closure s) ≤ Nat.card s := by
-  haveI := Fintype.ofFinite s
-  rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
-  exact rank_closure_finset_le_card s.toFinset
-
-theorem nat_card_centralizer_nat_card_stabilizer (g : G) :
-    Nat.card (Subgroup.centralizer {g}) =
-      Nat.card (MulAction.stabilizer (ConjAct G) g) := by
-  rw [Subgroup.centralizer_eq_comap_stabilizer]
-  rfl
-
-end Subgroup
-
 section QuotientGroup
 
 @[to_additive]

Mathlib/GroupTheory/Perm/Centralizer.lean

@@ -5,11 +5,11 @@ Authors: Antoine Chambert-Loir
 -/
 import Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
-import Mathlib.GroupTheory.Finiteness
 import Mathlib.GroupTheory.NoncommCoprod
 import Mathlib.GroupTheory.Perm.ConjAct
 import Mathlib.GroupTheory.Perm.Cycle.PossibleTypes
 import Mathlib.GroupTheory.Perm.DomMulAct
+import Mathlib.GroupTheory.Rank
 
 /-!
 # Centralizer of a permutation and cardinality of conjugacy classes in the symmetric groups

Mathlib/GroupTheory/Rank.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2025 Thomas Browning. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning
+-/
+import Mathlib.GroupTheory.Finiteness
+import Mathlib.SetTheory.Cardinal.Finite
+
+/-!
+# Rank of a group
+
+This file defines the rank of a group, namely the minimum size of a generating set.
+
+## TODO
+
+Should we define `erank G : ℕ∞` the rank of a not necessarily finitely generated group `G`,
+then redefine `rank G` as `(erank G).toNat`? Maybe a `Cardinal`-valued version too?
+-/
+
+open Function Group
+
+variable {G H : Type*} [Group G] [Group H]
+
+namespace Group
+
+variable (G) in
+/-- The minimum number of generators of a group. -/
+@[to_additive "The minimum number of generators of an additive group."]
+noncomputable def rank [h : FG G] : ℕ := @Nat.find _ (Classical.decPred _) (fg_iff'.mp h)
+
+variable (G) in
+@[to_additive]
+lemma rank_spec [h : FG G] : ∃ S : Finset G, S.card = rank G ∧ .closure S = (⊤ : Subgroup G) :=
+  @Nat.find_spec _ (Classical.decPred _) (fg_iff'.mp h)
+
+@[to_additive]
+lemma rank_le [h : FG G] {S : Finset G} (hS : .closure S = (⊤ : Subgroup G)) : rank G ≤ S.card :=
+  @Nat.find_le _ _ (Classical.decPred _) (fg_iff'.mp h) ⟨S, rfl, hS⟩
+
+@[to_additive]
+lemma rank_le_of_surjective [FG G] [FG H] (f : G →* H) (hf : Surjective f) : rank H ≤ rank G := by
+  classical
+  obtain ⟨S, hS1, hS2⟩ := rank_spec G
+  trans (S.image f).card
+  · apply rank_le
+    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]
+  · exact Finset.card_image_le.trans_eq hS1
+
+@[to_additive]
+lemma rank_range_le [FG G] {f : G →* H} : rank f.range ≤ rank G :=
+  rank_le_of_surjective f.rangeRestrict f.rangeRestrict_surjective
+
+@[to_additive]
+lemma rank_congr [FG G] [FG H] (e : G ≃* H) : rank G = rank H :=
+  le_antisymm (rank_le_of_surjective e.symm e.symm.surjective)
+    (rank_le_of_surjective e e.surjective)
+
+end Group
+
+namespace Subgroup
+
+@[to_additive]
+lemma rank_congr {H K : Subgroup G} [Group.FG H] [Group.FG K] (h : H = K) : rank H = rank K := by
+  subst h; rfl
+
+@[to_additive]
+lemma rank_closure_finset_le_card (s : Finset G) : rank (closure (s : Set G)) ≤ s.card := by
+  classical
+  let t : Finset (closure (s : Set G)) := s.preimage Subtype.val Subtype.coe_injective.injOn
+  have ht : closure (t : Set (closure (s : Set G))) = ⊤ := by
+    rw [Finset.coe_preimage]
+    exact closure_preimage_eq_top (s : Set G)
+  apply (rank_le ht).trans
+  suffices H : Set.InjOn Subtype.val (t : Set (closure (s : Set G))) by
+    rw [← Finset.card_image_of_injOn H, Finset.image_preimage]
+    apply Finset.card_filter_le
+  apply Subtype.coe_injective.injOn
+
+@[to_additive]
+lemma rank_closure_finite_le_nat_card (s : Set G) [Finite s] : rank (closure s) ≤ Nat.card s := by
+  haveI := Fintype.ofFinite s
+  rw [Nat.card_eq_fintype_card, ← s.toFinset_card, ← rank_congr (congr_arg _ s.coe_toFinset)]
+  exact rank_closure_finset_le_card s.toFinset
+
+lemma nat_card_centralizer_nat_card_stabilizer (g : G) :
+    Nat.card (centralizer {g}) = Nat.card (MulAction.stabilizer (ConjAct G) g) := by
+  rw [centralizer_eq_comap_stabilizer];   rfl
+
+end Subgroup

Mathlib/GroupTheory/Schreier.lean

@@ -159,7 +159,7 @@ theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] :
   obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G
   obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS
   calc
-    Group.rank H ≤ #T := Group.rank_le H hT
+    Group.rank H ≤ #T := Group.rank_le hT
     _ ≤ H.index * #S := hT₀
     _ = H.index * Group.rank G := congr_arg (H.index * ·) hS₀
 

Mathlib/NumberTheory/PellMatiyasevic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.Nat.Prime.Basic
 import Mathlib.NumberTheory.Zsqrtd.Basic