Finitely generated monoids and groups #

We define finitely generated monoids and groups. See also Submodule.FG and Module.Finite for finitely-generated modules.

Main definition #

Submonoid.FG S, AddSubmonoid.FG S : A submonoid S is finitely generated.
Monoid.FG M, AddMonoid.FG M : A typeclass indicating a type M is finitely generated as a monoid.
Subgroup.FG S, AddSubgroup.FG S : A subgroup S is finitely generated.
Group.FG M, AddGroup.FG M : A typeclass indicating a type M is finitely generated as a group.

Monoids and submonoids #

source

def AddSubmonoid.FG {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) :

Prop

An additive submonoid of N is finitely generated if it is the closure of a finite subset of M.

Equations

AddSubmonoid.FG P = ∃ S, AddSubmonoid.closure ↑S = P

Instances For

source

def Submonoid.FG {M : Type u_1} [Monoid M] (P : Submonoid M) :

Prop

A submonoid of M is finitely generated if it is the closure of a finite subset of M.

Equations

Submonoid.FG P = ∃ S, Submonoid.closure ↑S = P

Instances For

source

abbrev AddSubmonoid.fg_iff.match_1 {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) (motive : AddSubmonoid.FG P → Prop) :

(x : AddSubmonoid.FG P) → ((S : Finset M) → (hS : AddSubmonoid.closure ↑S = P) → motive (_ : ∃ S, AddSubmonoid.closure ↑S = P)) → motive x

Equations

AddSubmonoid.fg_iff.match_1 P motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

source

theorem AddSubmonoid.fg_iff {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) :

AddSubmonoid.FG P ↔ ∃ S, AddSubmonoid.closure S = P ∧ Set.Finite S

An equivalent expression of AddSubmonoid.FG in terms of Set.Finite instead of Finset.

source

abbrev AddSubmonoid.fg_iff.match_2 {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) (motive : (∃ S, AddSubmonoid.closure S = P ∧ Set.Finite S) → Prop) :

(x : ∃ S, AddSubmonoid.closure S = P ∧ Set.Finite S) → ((S : Set M) → (hS : AddSubmonoid.closure S = P) → (hf : Set.Finite S) → motive (_ : ∃ S, AddSubmonoid.closure S = P ∧ Set.Finite S)) → motive x

Equations

AddSubmonoid.fg_iff.match_2 P motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

Instances For

source

theorem Submonoid.fg_iff {M : Type u_1} [Monoid M] (P : Submonoid M) :

Submonoid.FG P ↔ ∃ S, Submonoid.closure S = P ∧ Set.Finite S

An equivalent expression of Submonoid.FG in terms of Set.Finite instead of Finset.

source

theorem Submonoid.fg_iff_add_fg {M : Type u_1} [Monoid M] (P : Submonoid M) :

Submonoid.FG P ↔ AddSubmonoid.FG (↑Submonoid.toAddSubmonoid P)

source

theorem AddSubmonoid.fg_iff_mul_fg {N : Type u_2} [AddMonoid N] (P : AddSubmonoid N) :

AddSubmonoid.FG P ↔ Submonoid.FG (↑AddSubmonoid.toSubmonoid P)

source

class Monoid.FG (M : Type u_1) [Monoid M] :

Prop

out : Submonoid.FG ⊤

A monoid is finitely generated if it is finitely generated as a submonoid of itself.

Instances

source

class AddMonoid.FG (N : Type u_2) [AddMonoid N] :

Prop

out : AddSubmonoid.FG ⊤

An additive monoid is finitely generated if it is finitely generated as an additive submonoid of itself.

Instances

source

theorem Monoid.fg_def {M : Type u_1} [Monoid M] :

Monoid.FG M ↔ Submonoid.FG ⊤

source

theorem AddMonoid.fg_def {N : Type u_2} [AddMonoid N] :

AddMonoid.FG N ↔ AddSubmonoid.FG ⊤

source

theorem AddMonoid.fg_iff {M : Type u_1} [AddMonoid M] :

AddMonoid.FG M ↔ ∃ S, AddSubmonoid.closure S = ⊤ ∧ Set.Finite S

An equivalent expression of AddMonoid.FG in terms of Set.Finite instead of Finset.

source

theorem Monoid.fg_iff {M : Type u_1} [Monoid M] :

Monoid.FG M ↔ ∃ S, Submonoid.closure S = ⊤ ∧ Set.Finite S

An equivalent expression of Monoid.FG in terms of Set.Finite instead of Finset.

source

theorem Monoid.fg_iff_add_fg {M : Type u_1} [Monoid M] :

Monoid.FG M ↔ AddMonoid.FG (Additive M)

source

theorem AddMonoid.fg_iff_mul_fg {N : Type u_2} [AddMonoid N] :

AddMonoid.FG N ↔ Monoid.FG (Multiplicative N)

source

instance AddMonoid.fg_of_monoid_fg {M : Type u_1} [Monoid M] [Monoid.FG M] :

AddMonoid.FG (Additive M)

Equations

@AddMonoid.fg_of_monoid_fg = @AddMonoid.fg_of_monoid_fg.proof_1

source

instance Monoid.fg_of_addMonoid_fg {N : Type u_2} [AddMonoid N] [AddMonoid.FG N] :

Monoid.FG (Multiplicative N)

Equations

@Monoid.fg_of_addMonoid_fg = @Monoid.fg_of_addMonoid_fg.proof_1

source

theorem AddMonoid.fg_of_finite.proof_1 {M : Type u_1} [AddMonoid M] [Finite M] :

AddMonoid.FG M

source

instance AddMonoid.fg_of_finite {M : Type u_1} [AddMonoid M] [Finite M] :

AddMonoid.FG M

Equations

@AddMonoid.fg_of_finite = @AddMonoid.fg_of_finite.proof_1

source

instance Monoid.fg_of_finite {M : Type u_1} [Monoid M] [Finite M] :

Monoid.FG M

Equations

@Monoid.fg_of_finite = @Monoid.fg_of_finite.proof_1

source

theorem AddSubmonoid.FG.map {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] {P : AddSubmonoid M} (h : AddSubmonoid.FG P) (e : M →+ M') :

AddSubmonoid.FG (AddSubmonoid.map e P)

source

theorem Submonoid.FG.map {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] {P : Submonoid M} (h : Submonoid.FG P) (e : M →* M') :

Submonoid.FG (Submonoid.map e P)

source

theorem AddSubmonoid.FG.map_injective {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] {P : AddSubmonoid M} (e : M →+ M') (he : Function.Injective ↑e) (h : AddSubmonoid.FG (AddSubmonoid.map e P)) :

AddSubmonoid.FG P

source

theorem Submonoid.FG.map_injective {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] {P : Submonoid M} (e : M →* M') (he : Function.Injective ↑e) (h : Submonoid.FG (Submonoid.map e P)) :

Submonoid.FG P

source

@[simp]

theorem AddMonoid.fg_iff_addSubmonoid_fg {M : Type u_1} [AddMonoid M] (N : AddSubmonoid M) :

AddMonoid.FG { x // x ∈ N } ↔ AddSubmonoid.FG N

source

@[simp]

theorem Monoid.fg_iff_submonoid_fg {M : Type u_1} [Monoid M] (N : Submonoid M) :

Monoid.FG { x // x ∈ N } ↔ Submonoid.FG N

source

theorem AddMonoid.fg_of_surjective {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] [AddMonoid.FG M] (f : M →+ M') (hf : Function.Surjective ↑f) :

AddMonoid.FG M'

source

theorem Monoid.fg_of_surjective {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [Monoid.FG M] (f : M →* M') (hf : Function.Surjective ↑f) :

Monoid.FG M'

source

instance AddMonoid.fg_range {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] [AddMonoid.FG M] (f : M →+ M') :

AddMonoid.FG { x // x ∈ AddMonoidHom.mrange f }

Equations

@AddMonoid.fg_range = @AddMonoid.fg_range.proof_1

source

theorem AddMonoid.fg_range.proof_1 {M : Type u_1} [AddMonoid M] {M' : Type u_2} [AddMonoid M'] [AddMonoid.FG M] (f : M →+ M') :

AddMonoid.FG { x // x ∈ AddMonoidHom.mrange f }

source

instance Monoid.fg_range {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [Monoid.FG M] (f : M →* M') :

Monoid.FG { x // x ∈ MonoidHom.mrange f }

Equations

@Monoid.fg_range = @Monoid.fg_range.proof_1

source

theorem AddSubmonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) :

AddSubmonoid.FG (AddSubmonoid.multiples r)

source

theorem Submonoid.powers_fg {M : Type u_1} [Monoid M] (r : M) :

Submonoid.FG (Submonoid.powers r)

source

instance AddMonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) :

AddMonoid.FG { x // x ∈ AddSubmonoid.multiples r }

Equations

@AddMonoid.multiples_fg = @AddMonoid.multiples_fg.proof_1

source

theorem AddMonoid.multiples_fg.proof_1 {M : Type u_1} [AddMonoid M] (r : M) :

AddMonoid.FG { x // x ∈ AddSubmonoid.multiples r }

source

instance Monoid.powers_fg {M : Type u_1} [Monoid M] (r : M) :

Monoid.FG { x // x ∈ Submonoid.powers r }

Equations

@Monoid.powers_fg = @Monoid.powers_fg.proof_1

source

theorem AddMonoid.closure_finset_fg.proof_1 {M : Type u_1} [AddMonoid M] (s : Finset M) :

AddMonoid.FG { x // x ∈ AddSubmonoid.closure ↑s }

source

instance AddMonoid.closure_finset_fg {M : Type u_1} [AddMonoid M] (s : Finset M) :

AddMonoid.FG { x // x ∈ AddSubmonoid.closure ↑s }

Equations

@AddMonoid.closure_finset_fg = @AddMonoid.closure_finset_fg.proof_1

source

instance Monoid.closure_finset_fg {M : Type u_1} [Monoid M] (s : Finset M) :

Monoid.FG { x // x ∈ Submonoid.closure ↑s }

Equations

@Monoid.closure_finset_fg = @Monoid.closure_finset_fg.proof_1

source

instance AddMonoid.closure_finite_fg {M : Type u_1} [AddMonoid M] (s : Set M) [Finite ↑s] :

AddMonoid.FG { x // x ∈ AddSubmonoid.closure s }

Equations

@AddMonoid.closure_finite_fg = @AddMonoid.closure_finite_fg.proof_1

source

theorem AddMonoid.closure_finite_fg.proof_1 {M : Type u_1} [AddMonoid M] (s : Set M) [Finite ↑s] :

AddMonoid.FG { x // x ∈ AddSubmonoid.closure s }

source

instance Monoid.closure_finite_fg {M : Type u_1} [Monoid M] (s : Set M) [Finite ↑s] :

Monoid.FG { x // x ∈ Submonoid.closure s }

Equations

@Monoid.closure_finite_fg = @Monoid.closure_finite_fg.proof_1

Groups and subgroups #

source

def AddSubgroup.FG {G : Type u_3} [AddGroup G] (P : AddSubgroup G) :

Prop

An additive subgroup of H is finitely generated if it is the closure of a finite subset of H.

Equations

AddSubgroup.FG P = ∃ S, AddSubgroup.closure ↑S = P

Instances For

source

def Subgroup.FG {G : Type u_3} [Group G] (P : Subgroup G) :

Prop

A subgroup of G is finitely generated if it is the closure of a finite subset of G.

Equations

Subgroup.FG P = ∃ S, Subgroup.closure ↑S = P

Instances For

source

abbrev AddSubgroup.fg_iff.match_1 {G : Type u_1} [AddGroup G] (P : AddSubgroup G) (motive : AddSubgroup.FG P → Prop) :

(x : AddSubgroup.FG P) → ((S : Finset G) → (hS : AddSubgroup.closure ↑S = P) → motive (_ : ∃ S, AddSubgroup.closure ↑S = P)) → motive x

Equations

AddSubgroup.fg_iff.match_1 P motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

source

theorem AddSubgroup.fg_iff {G : Type u_3} [AddGroup G] (P : AddSubgroup G) :

AddSubgroup.FG P ↔ ∃ S, AddSubgroup.closure S = P ∧ Set.Finite S

An equivalent expression of AddSubgroup.fg in terms of Set.Finite instead of Finset.

source

abbrev AddSubgroup.fg_iff.match_2 {G : Type u_1} [AddGroup G] (P : AddSubgroup G) (motive : (∃ S, AddSubgroup.closure S = P ∧ Set.Finite S) → Prop) :

(x : ∃ S, AddSubgroup.closure S = P ∧ Set.Finite S) → ((S : Set G) → (hS : AddSubgroup.closure S = P) → (hf : Set.Finite S) → motive (_ : ∃ S, AddSubgroup.closure S = P ∧ Set.Finite S)) → motive x

Equations

AddSubgroup.fg_iff.match_2 P motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

Instances For

source

theorem Subgroup.fg_iff {G : Type u_3} [Group G] (P : Subgroup G) :

Subgroup.FG P ↔ ∃ S, Subgroup.closure S = P ∧ Set.Finite S

An equivalent expression of Subgroup.FG in terms of Set.Finite instead of Finset.

source

theorem AddSubgroup.fg_iff_addSubmonoid_fg {G : Type u_3} [AddGroup G] (P : AddSubgroup G) :

AddSubgroup.FG P ↔ AddSubmonoid.FG P.toAddSubmonoid

An additive subgroup is finitely generated if and only if it is finitely generated as an additive submonoid.

source

theorem Subgroup.fg_iff_submonoid_fg {G : Type u_3} [Group G] (P : Subgroup G) :

Subgroup.FG P ↔ Submonoid.FG P.toSubmonoid

A subgroup is finitely generated if and only if it is finitely generated as a submonoid.

source

theorem Subgroup.fg_iff_add_fg {G : Type u_3} [Group G] (P : Subgroup G) :

Subgroup.FG P ↔ AddSubgroup.FG (↑Subgroup.toAddSubgroup P)

source

theorem AddSubgroup.fg_iff_mul_fg {H : Type u_4} [AddGroup H] (P : AddSubgroup H) :

AddSubgroup.FG P ↔ Subgroup.FG (↑AddSubgroup.toSubgroup P)

source

class Group.FG (G : Type u_3) [Group G] :

Prop

out : Subgroup.FG ⊤

A group is finitely generated if it is finitely generated as a submonoid of itself.

Instances

source

class AddGroup.FG (H : Type u_4) [AddGroup H] :

Prop

out : AddSubgroup.FG ⊤

An additive group is finitely generated if it is finitely generated as an additive submonoid of itself.

Instances

source

theorem Group.fg_def {G : Type u_3} [Group G] :

Group.FG G ↔ Subgroup.FG ⊤

source

theorem AddGroup.fg_def {H : Type u_4} [AddGroup H] :

AddGroup.FG H ↔ AddSubgroup.FG ⊤

source

theorem AddGroup.fg_iff {G : Type u_3} [AddGroup G] :

AddGroup.FG G ↔ ∃ S, AddSubgroup.closure S = ⊤ ∧ Set.Finite S

An equivalent expression of AddGroup.fg in terms of Set.Finite instead of Finset.

source

theorem Group.fg_iff {G : Type u_3} [Group G] :

Group.FG G ↔ ∃ S, Subgroup.closure S = ⊤ ∧ Set.Finite S

An equivalent expression of Group.FG in terms of Set.Finite instead of Finset.

source

abbrev AddGroup.fg_iff'.match_1 {G : Type u_1} [AddGroup G] (motive : AddSubgroup.FG ⊤ → Prop) :

(x : AddSubgroup.FG ⊤) → ((S : Finset G) → (hS : AddSubgroup.closure ↑S = ⊤) → motive (_ : ∃ S, AddSubgroup.closure ↑S = ⊤)) → motive x

Equations

AddGroup.fg_iff'.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

source

theorem AddGroup.fg_iff' {G : Type u_3} [AddGroup G] :

AddGroup.FG G ↔ ∃ n S, Finset.card S = n ∧ AddSubgroup.closure ↑S = ⊤

source

abbrev AddGroup.fg_iff'.match_2 {G : Type u_1} [AddGroup G] (motive : (∃ n S, Finset.card S = n ∧ AddSubgroup.closure ↑S = ⊤) → Prop) :

(x : ∃ n S, Finset.card S = n ∧ AddSubgroup.closure ↑S = ⊤) → ((_n : ℕ) → (S : Finset G) → (_hn : Finset.card S = _n) → (hS : AddSubgroup.closure ↑S = ⊤) → motive (_ : ∃ n S, Finset.card S = n ∧ AddSubgroup.closure ↑S = ⊤)) → motive x

Equations

AddGroup.fg_iff'.match_2 motive x h_1 = Exists.casesOn x fun w h => Exists.casesOn h fun w_1 h => And.casesOn h fun left right => h_1 w w_1 left right

Instances For

source

theorem Group.fg_iff' {G : Type u_3} [Group G] :

Group.FG G ↔ ∃ n S, Finset.card S = n ∧ Subgroup.closure ↑S = ⊤

source

theorem AddGroup.fg_iff_addMonoid_fg {G : Type u_3} [AddGroup G] :

AddGroup.FG G ↔ AddMonoid.FG G

An additive group is finitely generated if and only if it is finitely generated as an additive monoid.

source

theorem Group.fg_iff_monoid_fg {G : Type u_3} [Group G] :

Group.FG G ↔ Monoid.FG G

A group is finitely generated if and only if it is finitely generated as a monoid.

source

@[simp]

theorem AddGroup.fg_iff_addSubgroup_fg {G : Type u_3} [AddGroup G] (H : AddSubgroup G) :

AddGroup.FG { x // x ∈ H } ↔ AddSubgroup.FG H

source

@[simp]

theorem Group.fg_iff_subgroup_fg {G : Type u_3} [Group G] (H : Subgroup G) :

Group.FG { x // x ∈ H } ↔ Subgroup.FG H

source

theorem GroupFG.iff_add_fg {G : Type u_3} [Group G] :

Group.FG G ↔ AddGroup.FG (Additive G)

source

theorem AddGroup.fg_iff_mul_fg {H : Type u_4} [AddGroup H] :

AddGroup.FG H ↔ Group.FG (Multiplicative H)

source

instance AddGroup.fg_of_group_fg {G : Type u_3} [Group G] [Group.FG G] :

AddGroup.FG (Additive G)

Equations

@AddGroup.fg_of_group_fg = @AddGroup.fg_of_group_fg.proof_1

source

instance Group.fg_of_mul_group_fg {H : Type u_4} [AddGroup H] [AddGroup.FG H] :

Group.FG (Multiplicative H)

Equations

@Group.fg_of_mul_group_fg = @Group.fg_of_mul_group_fg.proof_1

source

theorem AddGroup.fg_of_finite.proof_1 {G : Type u_1} [AddGroup G] [Finite G] :

AddGroup.FG G

source

instance AddGroup.fg_of_finite {G : Type u_3} [AddGroup G] [Finite G] :

AddGroup.FG G

Equations

@AddGroup.fg_of_finite = @AddGroup.fg_of_finite.proof_1

source

instance Group.fg_of_finite {G : Type u_3} [Group G] [Finite G] :

Group.FG G

Equations

@Group.fg_of_finite = @Group.fg_of_finite.proof_1

source

theorem AddGroup.fg_of_surjective {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [hG : AddGroup.FG G] {f : G →+ G'} (hf : Function.Surjective ↑f) :

AddGroup.FG G'

source

theorem Group.fg_of_surjective {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [hG : Group.FG G] {f : G →* G'} (hf : Function.Surjective ↑f) :

Group.FG G'

source

instance AddGroup.fg_range {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] (f : G →+ G') :

AddGroup.FG { x // x ∈ AddMonoidHom.range f }

Equations

@AddGroup.fg_range = @AddGroup.fg_range.proof_1

source

theorem AddGroup.fg_range.proof_1 {G : Type u_1} [AddGroup G] {G' : Type u_2} [AddGroup G'] [AddGroup.FG G] (f : G →+ G') :

AddGroup.FG { x // x ∈ AddMonoidHom.range f }

source

instance Group.fg_range {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] (f : G →* G') :

Group.FG { x // x ∈ MonoidHom.range f }

Equations

@Group.fg_range = @Group.fg_range.proof_1

source

instance AddGroup.closure_finset_fg {G : Type u_3} [AddGroup G] (s : Finset G) :

AddGroup.FG { x // x ∈ AddSubgroup.closure ↑s }

Equations

@AddGroup.closure_finset_fg = @AddGroup.closure_finset_fg.proof_1

source

theorem AddGroup.closure_finset_fg.proof_1 {G : Type u_1} [AddGroup G] (s : Finset G) :

AddGroup.FG { x // x ∈ AddSubgroup.closure ↑s }

source

instance Group.closure_finset_fg {G : Type u_3} [Group G] (s : Finset G) :

Group.FG { x // x ∈ Subgroup.closure ↑s }

Equations

@Group.closure_finset_fg = @Group.closure_finset_fg.proof_1

source

instance AddGroup.closure_finite_fg {G : Type u_3} [AddGroup G] (s : Set G) [Finite ↑s] :

AddGroup.FG { x // x ∈ AddSubgroup.closure s }

Equations

@AddGroup.closure_finite_fg = @AddGroup.closure_finite_fg.proof_1

source

theorem AddGroup.closure_finite_fg.proof_1 {G : Type u_1} [AddGroup G] (s : Set G) [Finite ↑s] :

AddGroup.FG { x // x ∈ AddSubgroup.closure s }

source

instance Group.closure_finite_fg {G : Type u_3} [Group G] (s : Set G) [Finite ↑s] :

Group.FG { x // x ∈ Subgroup.closure s }

Equations

@Group.closure_finite_fg = @Group.closure_finite_fg.proof_1

source

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

ℕ

The minimum number of generators of an additive group

Equations

AddGroup.rank G = Nat.find (_ : ∃ n S, Finset.card S = n ∧ AddSubgroup.closure ↑S = ⊤)

Instances For

source

theorem AddGroup.rank.proof_1 (G : Type u_1) [AddGroup G] [h : AddGroup.FG G] :

∃ n S, Finset.card S = n ∧ AddSubgroup.closure ↑S = ⊤

source

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

ℕ

The minimum number of generators of a group.

Equations

Group.rank G = Nat.find (_ : ∃ n S, Finset.card S = n ∧ Subgroup.closure ↑S = ⊤)

Instances For

source

theorem AddGroup.rank_spec (G : Type u_3) [AddGroup G] [h : AddGroup.FG G] :

∃ S, Finset.card S = AddGroup.rank G ∧ AddSubgroup.closure ↑S = ⊤

source

theorem Group.rank_spec (G : Type u_3) [Group G] [h : Group.FG G] :

∃ S, Finset.card S = Group.rank G ∧ Subgroup.closure ↑S = ⊤

source

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

AddGroup.rank G ≤ Finset.card S

source

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

Group.rank G ≤ Finset.card S

source

theorem AddGroup.rank_le_of_surjective {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] [AddGroup.FG G'] (f : G →+ G') (hf : Function.Surjective ↑f) :

AddGroup.rank G' ≤ AddGroup.rank G

source

theorem Group.rank_le_of_surjective {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] [Group.FG G'] (f : G →* G') (hf : Function.Surjective ↑f) :

Group.rank G' ≤ Group.rank G

source

theorem AddGroup.rank_range_le {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] {f : G →+ G'} :

AddGroup.rank { x // x ∈ AddMonoidHom.range f } ≤ AddGroup.rank G

source

theorem Group.rank_range_le {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] {f : G →* G'} :

Group.rank { x // x ∈ MonoidHom.range f } ≤ Group.rank G

source

theorem AddGroup.rank_congr {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] [AddGroup.FG G'] (f : G ≃+ G') :

AddGroup.rank G = AddGroup.rank G'

source

theorem Group.rank_congr {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] [Group.FG G'] (f : G ≃* G') :

Group.rank G = Group.rank G'

source

theorem AddSubgroup.rank_congr {G : Type u_3} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [AddGroup.FG { x // x ∈ H }] [AddGroup.FG { x // x ∈ K }] (h : H = K) :

AddGroup.rank { x // x ∈ H } = AddGroup.rank { x // x ∈ K }

source

theorem Subgroup.rank_congr {G : Type u_3} [Group G] {H : Subgroup G} {K : Subgroup G} [Group.FG { x // x ∈ H }] [Group.FG { x // x ∈ K }] (h : H = K) :

Group.rank { x // x ∈ H } = Group.rank { x // x ∈ K }

source

theorem AddSubgroup.rank_closure_finset_le_card {G : Type u_3} [AddGroup G] (s : Finset G) :

AddGroup.rank { x // x ∈ AddSubgroup.closure ↑s } ≤ Finset.card s

source

theorem Subgroup.rank_closure_finset_le_card {G : Type u_3} [Group G] (s : Finset G) :

Group.rank { x // x ∈ Subgroup.closure ↑s } ≤ Finset.card s

source

theorem AddSubgroup.rank_closure_finite_le_nat_card {G : Type u_3} [AddGroup G] (s : Set G) [Finite ↑s] :

AddGroup.rank { x // x ∈ AddSubgroup.closure s } ≤ Nat.card ↑s

source

theorem Subgroup.rank_closure_finite_le_nat_card {G : Type u_3} [Group G] (s : Set G) [Finite ↑s] :

Group.rank { x // x ∈ Subgroup.closure s } ≤ Nat.card ↑s

source

theorem QuotientAddGroup.fg.proof_1 {G : Type u_1} [AddGroup G] [AddGroup.FG G] (N : AddSubgroup G) [AddSubgroup.Normal N] :

AddGroup.FG (G ⧸ N)

source

instance QuotientAddGroup.fg {G : Type u_3} [AddGroup G] [AddGroup.FG G] (N : AddSubgroup G) [AddSubgroup.Normal N] :

AddGroup.FG (G ⧸ N)

Equations

@QuotientAddGroup.fg = @QuotientAddGroup.fg.proof_1

source

instance QuotientGroup.fg {G : Type u_3} [Group G] [Group.FG G] (N : Subgroup G) [Subgroup.Normal N] :

Group.FG (G ⧸ N)

Equations

@QuotientGroup.fg = @QuotientGroup.fg.proof_1