Structures · Algebra
Monoid.FG
A monoid is finitely generated if it is finitely generated as a submonoid of itself.
- Defined in
- Mathlib.GroupTheory.Finiteness
- Shape
- One type argument · adds fg_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances6
- Units
- FreeMonoid
- Algebra.GrothendieckGroup
- Subtype
- Prod
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- Monoid.FG.fg_top
- Monoid.fg_of_surjective
- IsLocalization.finiteType_of_monoid_fg
- Submonoid.exists_minimal_closure_eq_top
- finite_irreducible
- AddMonoid.fg_of_monoid_fg
- Pi.instMonoidFG
- Submonoid.closure_irreducible
- Prod.instMonoidFG
- AffineMonoid.to_twoUniqueProds
- Localization.fg
- Algebra.GrothendieckGroup.instFG
- IsLocalization.instFiniteTypeLocalizationOfFGSubtypeMemSubmonoid
- MonoidAlgebra.finiteType_of_fg
- Monoid.fg_range
Ancestors0
No ancestors.