Theorems · Theorem · group theory
AddSubmonoid.subset_closure
∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(AddSubmonoid.closure s)The AddSubmonoid generated by a set includes the set.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Basic
- Cited by
- 63 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
- Assumes
- AddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- SetLike.coestatement and proof · cited by 8,199
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement and proof · cited by 1,178
- AddSubmonoid.closurestatement · cited by 224
- AddSubmonoid.mem_closureproof · cited by 8
Cited by63
Results whose statement or proof uses this declaration.
- AddSubmonoid.closure_leproof · cited by 35
- AddSubmonoid.closure_inductionstatement and proof · cited by 30
- star_mul_self_nonnegproof · cited by 17
- AddSubmonoid.closure_monoproof · cited by 10
- AddSubgroup.fg_iff_addSubmonoid_fgproof · cited by 6
- AddSubgroup.closure_toAddSubmonoidproof · cited by 6
- AddSubmonoid.mem_closure_of_memproof · cited by 6
- Submodule.span_nat_eq_addSubmonoidClosureproof · cited by 5
- IsAddIndecomposable.mem_or_neg_mem_closure_baseOfproof · cited by 5
- FreeAddMonoid.closure_range_ofproof · cited by 3
- AddSubmonoid.closure_induction_leftstatement and proof · cited by 3
- AddSubmonoid.closure_singleton_eqproof · cited by 2