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