Theorems · Theorem · group theory
AddSubmonoid.FG.pi
∀ {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [inst : (i : ι) → AddMonoid (M i)] {P : (i : ι) → AddSubmonoid (M i)},
(∀ (i : ι), (P i).FG) → (AddSubmonoid.pi Set.univ P).FGFinite product of finitely generated additive submonoids is finitely generated.
- Defined in
- Mathlib.GroupTheory.Finiteness
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsetproof · cited by 13,712
- SetLike.coeproof · cited by 8,199
- Fintypeproof · cited by 7,736
- Set.univstatement and proof · cited by 3,945
- Finset.univproof · cited by 3,473
- Finitestatement and proof · cited by 3,029
- AddMonoidstatement and proof · cited by 2,864
- Set.iUnionproof · cited by 2,483
- iSupproof · cited by 2,415
- AddSubmonoidstatement and proof · cited by 1,178
- Finset.imageproof · cited by 910
Cited by1
Results whose statement or proof uses this declaration.
- AddSubgroup.FG.piproof · cited by 0