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?

noncomputable def Group.rank (G : Type u_1) [Group G] [h : FG G] : ℕ

The minimum number of generators of a group.

noncomputable def AddGroup.rank (G : Type u_1) [AddGroup G] [h : FG G] : ℕ

The minimum number of generators of an additive group.

theorem Group.rank_spec (G : Type u_1) [Group G] [h : FG G] : ∃ (S : Finset G), S.card = rank G ∧ Subgroup.closure ↑S = ⊤

theorem AddGroup.rank_spec (G : Type u_1) [AddGroup G] [h : FG G] : ∃ (S : Finset G), S.card = rank G ∧ AddSubgroup.closure ↑S = ⊤

theorem Group.rank_le {G : Type u_1} [Group G] [h : FG G] {S : Finset G} (hS : Subgroup.closure ↑S = ⊤) : rank G ≤ S.card

theorem AddGroup.rank_le {G : Type u_1} [AddGroup G] [h : FG G] {S : Finset G} (hS : AddSubgroup.closure ↑S = ⊤) : rank G ≤ S.card

theorem Group.rank_le_of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] [FG G] [FG H] (f : G →* H) (hf : Function.Surjective ⇑f) : rank H ≤ rank G

theorem AddGroup.rank_le_of_surjective {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [FG G] [FG H] (f : G →+ H) (hf : Function.Surjective ⇑f) : rank H ≤ rank G

theorem Group.rank_range_le {G : Type u_1} {H : Type u_2} [Group G] [Group H] [FG G] {f : G →* H} : rank ↥f.range ≤ rank G

theorem AddGroup.rank_range_le {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [FG G] {f : G →+ H} : rank ↥f.range ≤ rank G

theorem Group.rank_congr {G : Type u_1} {H : Type u_2} [Group G] [Group H] [FG G] [FG H] (e : G ≃* H) : rank G = rank H

theorem AddGroup.rank_congr {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [FG G] [FG H] (e : G ≃+ H) : rank G = rank H

theorem Subgroup.rank_congr {G : Type u_1} [Group G] {H K : Subgroup G} [Group.FG ↥H] [Group.FG ↥K] (h : H = K) : Group.rank ↥H = Group.rank ↥K

theorem AddSubgroup.rank_congr {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [AddGroup.FG ↥H] [AddGroup.FG ↥K] (h : H = K) : AddGroup.rank ↥H = AddGroup.rank ↥K

theorem Subgroup.rank_closure_finset_le_card {G : Type u_1} [Group G] (s : Finset G) : Group.rank ↥(closure ↑s) ≤ s.card

theorem AddSubgroup.rank_closure_finset_le_card {G : Type u_1} [AddGroup G] (s : Finset G) : AddGroup.rank ↥(closure ↑s) ≤ s.card

theorem Subgroup.rank_closure_finite_le_nat_card {G : Type u_1} [Group G] (s : Set G) [Finite ↑s] : Group.rank ↥(closure s) ≤ Nat.card ↑s

theorem AddSubgroup.rank_closure_finite_le_nat_card {G : Type u_1} [AddGroup G] (s : Set G) [Finite ↑s] : AddGroup.rank ↥(closure s) ≤ Nat.card ↑s

theorem Subgroup.nat_card_centralizer_nat_card_stabilizer {G : Type u_1} [Group G] (g : G) : Nat.card ↥(centralizer {g}) = Nat.card ↥(MulAction.stabilizer (ConjAct G) g)