Theorems · Theorem · group theory
AddSubmonoid.FG.sup
∀ {M : Type u_1} [inst : AddMonoid M] {P Q : AddSubmonoid M}, P.FG → Q.FG → (P ⊔ Q).FG- Defined in
- Mathlib.GroupTheory.Finiteness
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- AddMonoid
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.
- Finsetproof · cited by 13,712
- SetLike.coeproof · cited by 8,199
- AddMonoidstatement and proof · cited by 2,864
- AddSubmonoidstatement and proof · cited by 1,178
- AddSubmonoid.closureproof · cited by 224
- Finset.coe_unionproof · cited by 78
- AddSubmonoid.FGstatement and proof · cited by 36
- AddSubmonoid.closure_unionproof · cited by 10
Cited by2
Results whose statement or proof uses this declaration.
- IsSemilinearSet.exists_fg_eq_subtypeVal₂proof · cited by 2
- AddSubmonoid.FG.finset_supproof · cited by 1