Theorems · Theorem · group theory
Submonoid.mul_mem
∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ SA submonoid is closed under multiplication.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
- Assumes
- MulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Submonoidstatement and proof · cited by 3,086
- MulOneClassstatement and proof · cited by 1,018
- MulMemClass.mul_memproof · cited by 173
Cited by33
Results whose statement or proof uses this declaration.
- Algebra.adjoin_eq_spanproof · cited by 13
- Subgroup.closure_toSubmonoidproof · cited by 9
- RingHom.SurjectiveOnStalks.exists_mul_eq_tmulproof · cited by 4
- Submonoid.prod_le_iffproof · cited by 4
- IsFractional.mulproof · cited by 3
- RingHom.surjective_localRingHom_iffproof · cited by 3
- associatedPrimes.subset_union_of_exactproof · cited by 2
- IsFractional.div_of_nonzeroproof · cited by 1
- Subalgebra.saturation_saturationproof · cited by 1
- Submonoid.closure_mul_leproof · cited by 1
- Submonoid.top_closure_mul_self_subsetproof · cited by 1
- Ideal.isPrime_of_maximally_disjointproof · cited by 1