Structures · Algebra
AddGroup.FG
An additive group is finitely generated if it is finitely generated as an additive 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 instances7
- Int
- NumberField.RingOfIntegers
- FreeAddGroup
- Subtype
- Prod
- HasQuotient.Quotient
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by31
- AddGroup.rank
- AddCommGroup.freeRank
- AddGroup.FG.out
- AddGroup.rank_le
- AddGroup.rank_spec
- AddGroup.rank_le_of_surjective
- AddCommGroup.finite_of_fg_isAddTorsion
- AddGroup.rank_eq_zero_iff
- AddGroup.fg_of_surjective
- AddCommGroup.equiv_free_prod_directSum_zmod
- AddSubgroup.rank_congr
- AddCommGroup.freeRank_eq_zero
- AddSubgroup.finiteIndex_range_nsmulAddMonoidHom_of_fg
- card_dvd_exponent_nsmul_rank
- AddGroup.rank_congr
- AddCommGroup.freeRank_eq_zero_iff
- AddSubgroup.IsFinitelyNormallyGenerated.of_FG
- AddCommGroup.freeRank_congr
- AddCommGroup.finite_of_fg_torsion
- AddGroup.fg_range
- Group.fg_of_mul_group_fg
- AddGroup.rank_range_le
- Prod.instAddGroupFG
- AddCommGroup.freeRank_ge_of_surjective
- AddSubgroup.fg_of_index_ne_zero
- AddMonoid.fg_of_addGroup_fg
- AddCommGroup.freeRank_def
- AddGroup.rank_pos
- QuotientAddGroup.fg
- card_dvd_exponent_nsmul_rank'
- Pi.instAddGroupFG
Ancestors0
No ancestors.