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 submonoidS
is finitely generated.Monoid.FG M
,AddMonoid.FG M
: A typeclass indicating a typeM
is finitely generated as a monoid.Subgroup.FG S
,AddSubgroup.FG S
: A subgroupS
is finitely generated.Group.FG M
,AddGroup.FG M
: A typeclass indicating a typeM
is finitely generated as a group.
Monoids and submonoids #
A submonoid of M
is finitely generated if it is the closure of a finite subset of M
.
Instances For
An additive submonoid of N
is finitely generated if it is the closure of a finite subset of
M
.
Instances For
An equivalent expression of AddSubmonoid.FG
in terms of Set.Finite
instead of
Finset
.
An equivalent expression of Monoid.FG
in terms of Set.Finite
instead of Finset
.
An equivalent expression of AddMonoid.FG
in terms of Set.Finite
instead of Finset
.
Groups and subgroups #
A subgroup of G
is finitely generated if it is the closure of a finite subset of G
.
Instances For
An additive subgroup of H
is finitely generated if it is the closure of a finite subset of
H
.
Instances For
An additive subgroup is finitely generated if and only if it is finitely generated as an additive submonoid.
An equivalent expression of Group.FG
in terms of Set.Finite
instead of Finset
.
An equivalent expression of AddGroup.fg
in terms of Set.Finite
instead of Finset
.
An additive group is finitely generated if and only if it is finitely generated as an additive monoid.
The minimum number of generators of a group.
Instances For
The minimum number of generators of an additive group