Structures · Algebra
AddMonoid.FG
An additive monoid is finitely generated if it is finitely generated as an additive 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 instances7
- Nat
- FreeAbelianGroup
- FreeAddMonoid
- Algebra.GrothendieckAddGroup
- Subtype
- Prod
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- AddMonoid.FG.fg_top
- AddMonoid.fg_of_surjective
- IsSemilinearSet.sInter
- IsLinearSet.univ
- IsSemilinearSet.univ
- IsSemilinearSet.compl
- IsSemilinearSet.biInter
- AffineAddMonoid.embedding
- isSemilinearSet_setOfPred_eq
- AddSubmonoid.exists_minimal_closure_eq_top
- Monoid.fg_of_addMonoid_fg
- Algebra.GrothendieckAddGroup.instFG
- IsSemilinearSet.biInter_finset
- IsSemilinearSet.iInter
- AddMonoid.FG.to_moduleFinite_int
- IsSemilinearSet.preimage
- AddMonoidAlgebra.finiteType_of_fg
- AddMonoid.fg_range
- finite_addIrreducible
- Pi.instAddMonoidFG
- AffineAddMonoid.embedding_injective
- AffineAddMonoid.to_twoUniqueSums
- AddSubmonoid.closure_addIrreducible
- AddLocalization.fg
- AddMonoid.FG.to_moduleFinite_nat
- isSemilinearSet_setOf_eq
- Prod.instAddMonoidFG
Ancestors0
No ancestors.