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

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.

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.

theorem Submonoid.fg_iff {M : Type u_1} [Monoid M] (P : Submonoid M) : P.FG ↔ ∃ (S : Set M), closure S = P ∧ S.Finite

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

theorem AddSubmonoid.fg_iff {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) : P.FG ↔ ∃ (S : Set M), closure S = P ∧ S.Finite

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

theorem Submonoid.FG.exists_minimal_closure_eq {M : Type u_1} [Monoid M] {P : Submonoid M} (hP : P.FG) : ∃ (S : Finset M), Minimal (fun (S : Finset M) => closure ↑S = P) S

A finitely generated submonoid has a minimal generating set.

theorem AddSubmonoid.FG.exists_minimal_closure_eq {M : Type u_1} [AddMonoid M] {P : AddSubmonoid M} (hP : P.FG) : ∃ (S : Finset M), Minimal (fun (S : Finset M) => closure ↑S = P) S

A finitely generated submonoid has a minimal generating set.

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

theorem AddSubmonoid.fg_iff_mul_fg {M : Type u_3} [AddMonoid M] (P : AddSubmonoid M) : P.FG ↔ (toSubmonoid P).FG

theorem Submonoid.FG.bot {M : Type u_1} [Monoid M] : ⊥.FG

theorem AddSubmonoid.FG.bot {M : Type u_1} [AddMonoid M] : ⊥.FG

theorem Submonoid.FG.sup {M : Type u_1} [Monoid M] {P Q : Submonoid M} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem AddSubmonoid.FG.sup {M : Type u_1} [AddMonoid M] {P Q : AddSubmonoid M} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem Submonoid.FG.finset_sup {M : Type u_1} [Monoid M] {ι : Type u_3} (s : Finset ι) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem AddSubmonoid.FG.finset_sup {M : Type u_1} [AddMonoid M] {ι : Type u_3} (s : Finset ι) (P : ι → AddSubmonoid M) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem Submonoid.FG.biSup_finset {M : Type u_1} [Monoid M] {ι : Type u_3} (s : Finset ι) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubmonoid.FG.biSup_finset {M : Type u_1} [AddMonoid M] {ι : Type u_3} (s : Finset ι) (P : ι → AddSubmonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Submonoid.FG.biSup {M : Type u_1} [Monoid M] {ι : Type u_3} {s : Set ι} (hs : s.Finite) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubmonoid.FG.biSup {M : Type u_1} [AddMonoid M] {ι : Type u_3} {s : Set ι} (hs : s.Finite) (P : ι → AddSubmonoid M) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Submonoid.FG.iSup {M : Type u_1} [Monoid M] {ι : Sort u_3} [Finite ι] (P : ι → Submonoid M) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

theorem AddSubmonoid.FG.iSup {M : Type u_1} [AddMonoid M] {ι : Sort u_3} [Finite ι] (P : ι → AddSubmonoid M) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

theorem Submonoid.FG.prod {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {P : Submonoid M} {Q : Submonoid N} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

The product of two finitely generated submonoids is finitely generated.

theorem AddSubmonoid.FG.prod {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] {P : AddSubmonoid M} {Q : AddSubmonoid N} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

The product of two finitely generated additive submonoids is finitely generated.

@[deprecated AddSubmonoid.FG.prod (since := "2025-08-28")]

theorem AddSubmonoid.FG.sum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] {P : AddSubmonoid M} {Q : AddSubmonoid N} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

Alias of AddSubmonoid.FG.prod.

---

The product of two finitely generated additive submonoids is finitely generated.

theorem Submonoid.iSup_map_mulSingle {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → Monoid (M i)] {P : (i : ι) → Submonoid (M i)} [DecidableEq ι] : ⨆ (i : ι), map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P

theorem AddSubmonoid.iSup_map_single {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → AddMonoid (M i)] {P : (i : ι) → AddSubmonoid (M i)} [DecidableEq ι] : ⨆ (i : ι), map (AddMonoidHom.single M i) (P i) = pi Set.univ P

theorem Submonoid.FG.pi {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → Monoid (M i)] {P : (i : ι) → Submonoid (M i)} (hP : ∀ (i : ι), (P i).FG) : (Submonoid.pi Set.univ P).FG

Finite product of finitely generated submonoids is finitely generated.

theorem AddSubmonoid.FG.pi {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [(i : ι) → AddMonoid (M i)] {P : (i : ι) → AddSubmonoid (M i)} (hP : ∀ (i : ι), (P i).FG) : (AddSubmonoid.pi Set.univ P).FG

Finite product of finitely generated additive submonoids is finitely generated.

class AddMonoid.FG (M : Type u_3) [AddMonoid M] : Prop

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

• fg_top : ⊤.FG

theorem AddMonoid.fG_iff (M : Type u_3) [AddMonoid M] : FG M ↔ ⊤.FG

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

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

• fg_top : ⊤.FG

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

theorem AddMonoid.fg_def {M : Type u_1} [AddMonoid M] : FG M ↔ ⊤.FG

theorem Monoid.fg_iff {M : Type u_1} [Monoid M] : FG M ↔ ∃ (S : Set M), Submonoid.closure S = ⊤ ∧ S.Finite

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

theorem AddMonoid.fg_iff {M : Type u_1} [AddMonoid M] : FG M ↔ ∃ (S : Set M), AddSubmonoid.closure S = ⊤ ∧ S.Finite

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

theorem Monoid.fg_iff_exists_freeMonoid_hom_surjective {M : Type u_1} [Monoid M] : FG M ↔ ∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid ↑S →* M), Function.Surjective ⇑φ

A monoid is finitely generated iff there exists a surjective homomorphism from a FreeMonoid on finitely many generators.

theorem AddMonoid.fg_iff_exists_freeAddMonoid_hom_surjective {M : Type u_1} [AddMonoid M] : FG M ↔ ∃ (S : Set M) (_ : S.Finite) (φ : FreeAddMonoid ↑S →+ M), Function.Surjective ⇑φ

An additive monoid is finitely generated iff there exists a surjective homomorphism from a FreeAddMonoid on finitely many generators.

theorem Submonoid.exists_minimal_closure_eq_top (M : Type u_1) [Monoid M] [Monoid.FG M] : ∃ (S : Finset M), Minimal (fun (S : Finset M) => closure ↑S = ⊤) S

A finitely generated monoid has a minimal generating set.

theorem AddSubmonoid.exists_minimal_closure_eq_top (M : Type u_1) [AddMonoid M] [AddMonoid.FG M] : ∃ (S : Finset M), Minimal (fun (S : Finset M) => closure ↑S = ⊤) S

A finitely generated monoid has a minimal generating set.

theorem Monoid.fg_iff_add_fg {M : Type u_1} [Monoid M] : FG M ↔ AddMonoid.FG (Additive M)

theorem AddMonoid.fg_iff_mul_fg {M : Type u_3} [AddMonoid M] : FG M ↔ Monoid.FG (Multiplicative M)

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

instance Monoid.fg_of_addMonoid_fg {M : Type u_3} [AddMonoid M] [AddMonoid.FG M] : FG (Multiplicative M)

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

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

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

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

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.map e P).FG) : P.FG

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.map e P).FG) : P.FG

@[simp]

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

@[simp]

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

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

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

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

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

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

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

instance Monoid.powers_fg {M : Type u_1} [Monoid M] (r : M) : FG ↥(Submonoid.powers r)

instance AddMonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) : FG ↥(AddSubmonoid.multiples r)

instance Monoid.closure_finset_fg {M : Type u_1} [Monoid M] (s : Finset M) : FG ↥(Submonoid.closure ↑s)

instance AddMonoid.closure_finset_fg {M : Type u_1} [AddMonoid M] (s : Finset M) : FG ↥(AddSubmonoid.closure ↑s)

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

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

Groups and subgroups

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.

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.

theorem Subgroup.fg_iff {G : Type u_3} [Group G] (P : Subgroup G) : P.FG ↔ ∃ (S : Set G), closure S = P ∧ S.Finite

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

theorem AddSubgroup.fg_iff {G : Type u_3} [AddGroup G] (P : AddSubgroup G) : P.FG ↔ ∃ (S : Set G), closure S = P ∧ S.Finite

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

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

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

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

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

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

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

theorem Subgroup.FG.bot {G : Type u_3} [Group G] : ⊥.FG

theorem AddSubgroup.FG.bot {G : Type u_3} [AddGroup G] : ⊥.FG

theorem Subgroup.FG.sup {G : Type u_3} [Group G] {P Q : Subgroup G} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem AddSubgroup.FG.sup {G : Type u_3} [AddGroup G] {P Q : AddSubgroup G} (hP : P.FG) (hQ : Q.FG) : (P ⊔ Q).FG

theorem Subgroup.FG.finset_sup {G : Type u_3} [Group G] {ι : Type u_5} (s : Finset ι) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem AddSubgroup.FG.finset_sup {G : Type u_3} [AddGroup G] {ι : Type u_5} (s : Finset ι) (P : ι → AddSubgroup G) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG

theorem Subgroup.FG.biSup_finset {G : Type u_3} [Group G] {ι : Type u_5} (s : Finset ι) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubgroup.FG.biSup_finset {G : Type u_3} [AddGroup G] {ι : Type u_5} (s : Finset ι) (P : ι → AddSubgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Subgroup.FG.biSup {G : Type u_3} [Group G] {ι : Type u_5} {s : Set ι} (hs : s.Finite) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem AddSubgroup.FG.biSup {G : Type u_3} [AddGroup G] {ι : Type u_5} {s : Set ι} (hs : s.Finite) (P : ι → AddSubgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG

theorem Subgroup.FG.iSup {G : Type u_3} [Group G] {ι : Sort u_5} [Finite ι] (P : ι → Subgroup G) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

theorem AddSubgroup.FG.iSup {G : Type u_3} [AddGroup G] {ι : Sort u_5} [Finite ι] (P : ι → AddSubgroup G) (hP : ∀ (i : ι), (P i).FG) : (_root_.iSup P).FG

theorem Subgroup.FG.prod {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] {P : Subgroup G} {Q : Subgroup G'} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

The product of two finitely generated subgroups is finitely generated.

theorem AddSubgroup.FG.prod {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] {P : AddSubgroup G} {Q : AddSubgroup G'} (hP : P.FG) (hQ : Q.FG) : (P.prod Q).FG

The product of two finitely generated additive subgroups is finitely generated.

theorem Subgroup.FG.pi {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [(i : ι) → Group (G i)] {P : (i : ι) → Subgroup (G i)} (hP : ∀ (i : ι), (P i).FG) : (Subgroup.pi Set.univ P).FG

Finite product of finitely generated subgroups is finitely generated.

theorem AddSubgroup.FG.pi {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [(i : ι) → AddGroup (G i)] {P : (i : ι) → AddSubgroup (G i)} (hP : ∀ (i : ι), (P i).FG) : (AddSubgroup.pi Set.univ P).FG

Finite product of finitely generated additive subgroups is finitely generated.

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

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

• out : ⊤.FG

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

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

• out : ⊤.FG

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

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

theorem Group.fg_iff {G : Type u_3} [Group G] : FG G ↔ ∃ (S : Set G), Subgroup.closure S = ⊤ ∧ S.Finite

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

theorem AddGroup.fg_iff {G : Type u_3} [AddGroup G] : FG G ↔ ∃ (S : Set G), AddSubgroup.closure S = ⊤ ∧ S.Finite

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

theorem Group.fg_iff' {G : Type u_3} [Group G] : FG G ↔ ∃ (n : ℕ) (S : Finset G), S.card = n ∧ Subgroup.closure ↑S = ⊤

theorem AddGroup.fg_iff' {G : Type u_3} [AddGroup G] : FG G ↔ ∃ (n : ℕ) (S : Finset G), S.card = n ∧ AddSubgroup.closure ↑S = ⊤

theorem Group.fg_iff_exists_freeGroup_hom_surjective {G : Type u_3} [Group G] : FG G ↔ ∃ (S : Set G) (_ : S.Finite) (φ : FreeGroup ↑S →* G), Function.Surjective ⇑φ

A group is finitely generated iff there exists a surjective homomorphism from a FreeGroup on finitely many generators.

theorem AddGroup.fg_iff_exists_freeAddGroup_hom_surjective {G : Type u_3} [AddGroup G] : FG G ↔ ∃ (S : Set G) (_ : S.Finite) (φ : FreeAddGroup ↑S →+ G), Function.Surjective ⇑φ

An additive group is finitely generated iff there exists a surjective homomorphism from a FreeAddGroup on finitely many generators.

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

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

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

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

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

instance AddMonoid.fg_of_addGroup_fg {G : Type u_3} [AddGroup G] [AddGroup.FG G] : FG G

@[simp]

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

@[simp]

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

theorem GroupFG.iff_add_fg {G : Type u_3} [Group G] : Group.FG G ↔ AddGroup.FG (Additive G)

theorem AddGroup.fg_iff_mul_fg {H : Type u_4} [AddGroup H] : FG H ↔ Group.FG (Multiplicative H)

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

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

@[instance 100]

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

@[instance 100]

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

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

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

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

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

instance Group.closure_finset_fg {G : Type u_3} [Group G] (s : Finset G) : FG ↥(Subgroup.closure ↑s)

instance AddGroup.closure_finset_fg {G : Type u_3} [AddGroup G] (s : Finset G) : FG ↥(AddSubgroup.closure ↑s)

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

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

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

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

instance Prod.instMonoidFG {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [Monoid.FG M] [Monoid.FG N] : Monoid.FG (M × N)

The product of two finitely generated monoids is finitely generated.

instance Prod.instAddMonoidFG {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] [AddMonoid.FG M] [AddMonoid.FG N] : AddMonoid.FG (M × N)

The product of two finitely generated additive monoids is finitely generated.

instance Prod.instGroupFG {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] [Group.FG G'] : Group.FG (G × G')

The product of two finitely generated groups is finitely generated.

instance Prod.instAddGroupFG {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] [AddGroup.FG G'] : AddGroup.FG (G × G')

The product of two finitely generated additive groups is finitely generated.

instance Pi.instMonoidFG {ι : Type u_5} [Finite ι] {M : ι → Type u_6} [(i : ι) → Monoid (M i)] [∀ (i : ι), Monoid.FG (M i)] : Monoid.FG ((i : ι) → M i)

Finite product of finitely generated monoids is finitely generated.

instance Pi.instAddMonoidFG {ι : Type u_5} [Finite ι] {M : ι → Type u_6} [(i : ι) → AddMonoid (M i)] [∀ (i : ι), AddMonoid.FG (M i)] : AddMonoid.FG ((i : ι) → M i)

Finite product of finitely generated additive monoids is finitely generated.

instance Pi.instGroupFG {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [(i : ι) → Group (G i)] [∀ (i : ι), Group.FG (G i)] : Group.FG ((i : ι) → G i)

Finite product of finitely generated groups is finitely generated.

instance Pi.instAddGroupFG {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [(i : ι) → AddGroup (G i)] [∀ (i : ι), AddGroup.FG (G i)] : AddGroup.FG ((i : ι) → G i)

Finite product of finitely generated additive groups is finitely generated.

instance AddMonoid.instFGNat : FG ℕ

instance AddGroup.instFGInt : FG ℤ

theorem Submonoid.fg_of_divisive {M : Type u_5} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M] [CanonicallyOrderedMul M] {P : Submonoid M} (hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P) : P.FG

In a canonically ordered and well-quasi-ordered monoid, any divisive submonoid is finitely generated.

theorem AddSubmonoid.fg_of_subtractive {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] {P : AddSubmonoid M} (hP : ∀ x ∈ P, ∀ (y : M), x + y ∈ P → y ∈ P) : P.FG

In a canonically ordered and well-quasi-ordered additive monoid (typical example is ℕ ^ k), any subtractive submonoid is finitely generated.

theorem CommMonoid.fg_of_wellQuasiOrderedLE {M : Type u_5} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M] [CanonicallyOrderedMul M] : Monoid.FG M

A canonically ordered and well-quasi-ordered monoid must be finitely generated.

theorem AddCommMonoid.fg_of_wellQuasiOrderedLE {M : Type u_5} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] : AddMonoid.FG M

A canonically ordered and well-quasi-ordered additive monoid must be finitely generated.

theorem Submonoid.fg_eqLocusM {M : Type u_5} {N : Type u_6} [CommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M] [CanonicallyOrderedMul M] [Monoid N] [IsCancelMul N] (f g : M →* N) : (f.eqLocusM g).FG

If f g are homomorphisms from a canonically ordered and well-quasi-ordered monoid M to a cancellative monoid N, the submonoid of M on which f and g agree is finitely generated.

theorem AddSubmonoid.fg_eqLocusM {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelAddMonoid M] [CanonicallyOrderedAdd M] [AddMonoid N] [IsCancelAdd N] (f g : M →+ N) : (f.eqLocusM g).FG

If f g are homomorphisms from a canonically ordered and well-quasi-ordered additive monoid M to a cancellative additive monoid N, the submonoid of M on which f and g agree is finitely generated. When M and N are ℕ ^ k, this is also known as a version of Gordan's lemma.