Theorems · Theorem · group theory
AddSubgroup.FG.pi
∀ {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [inst : (i : ι) → AddGroup (G i)] {P : (i : ι) → AddSubgroup (G i)},
(∀ (i : ι), (P i).FG) → (AddSubgroup.pi Set.univ P).FGFinite product of finitely generated additive subgroups is finitely generated.
- Defined in
- Mathlib.GroupTheory.Finiteness
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- Set.univstatement and proof · cited by 3,945
- AddSubgroupstatement and proof · cited by 3,232
- Finitestatement and proof · cited by 3,029
- AddSubgroup.pistatement and proof · cited by 26
- AddSubgroup.FGstatement and proof · cited by 21
- AddSubgroup.fg_iff_addSubmonoid_fgproof · cited by 6
- AddSubmonoid.FG.piproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.