Structures · Algebra
Group.FG
A group is finitely generated if it is finitely generated as a subgroup of itself.
- Defined in
- Mathlib.GroupTheory.Finiteness
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- FreeGroup
- Subtype
- Prod
- HasQuotient.Quotient
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by34
- Group.rank
- CommGroup.freeRank
- Group.rank_spec
- Group.rank_le
- Group.FG.out
- Group.rank_le_of_surjective
- Group.fg_of_surjective
- Group.rank_eq_zero_iff
- CommGroup.finite_of_fg_isMulTorsion
- Subgroup.rank_congr
- CommGroup.freeRank_eq_zero
- Subgroup.finiteIndex_range_powMonoidHom_of_fg
- Group.rank_congr
- card_dvd_exponent_pow_rank'
- Subgroup.IsFinitelyNormallyGenerated.of_FG
- Subgroup.index_center_le_pow
- CommGroup.freeRank_eq_zero_iff
- Subgroup.rank_le_index_mul_rank
- card_dvd_exponent_pow_rank
- Pi.instGroupFG
- Monoid.fg_of_group_fg
- Subgroup.fg_of_index_ne_zero
- Subgroup.finiteIndex_center
- AddGroup.fg_of_group_fg
- Group.rank_range_le
- QuotientGroup.fg
- CommGroup.freeRank_def
- Group.fg_range
- CommGroup.finite_of_fg_torsion
- CommGroup.freeRank_congr
- CommGroup.freeRank_ge_of_surjective
- Prod.instGroupFG
- Group.rank_pos
- CommGroup.equiv_free_prod_prod_multiplicative_zmod
Ancestors0
No ancestors.