Theorems · Inductive type · group theory
AddGroup.FG
(H : Type u_4) → [AddGroup H] → Prop
An additive group is finitely generated if it is finitely generated as an additive subgroup of itself.
- Defined in
- Mathlib.GroupTheory.Finiteness
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- AddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement · cited by 4,410
Cited by41
Results whose statement or proof uses this declaration.
- AddGroup.rankstatement and proof · cited by 14
- AddCommGroup.freeRankstatement and proof · cited by 6
- AddGroup.FG.outstatement and proof · cited by 4
- AddGroup.rank_lestatement and proof · cited by 3
- AddGroup.rank_le_of_surjectivestatement and proof · cited by 3
- AddGroup.rank_specstatement and proof · cited by 3
- AddGroup.fg_defstatement and proof · cited by 3
- AddCommGroup.equiv_free_prod_directSum_zmodstatement and proof · cited by 2
- AddCommGroup.finite_of_fg_isAddTorsionstatement and proof · cited by 2
- AddGroup.rank_eq_zero_iffstatement and proof · cited by 2
- AddGroup.fg_iff_addMonoid_fgstatement and proof · cited by 2
- AddGroup.fg_iff_addSubgroup_fgstatement · cited by 2