Theorems · Theorem · group theory
Submonoid.one_mem
∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), 1 ∈ SA submonoid contains the monoid's 1.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 28 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
- OneMemClass.one_memproof · cited by 87
Cited by28
Results whose statement or proof uses this declaration.
- IsLocalization.AtPrime.isLocalRingproof · cited by 19
- Subgroup.closure_toSubmonoidproof · cited by 9
- IsLocalization.disjoint_under_iffproof · cited by 6
- isIntegral_localizationproof · cited by 4
- RingHom.SurjectiveOnStalks.exists_mul_eq_tmulproof · cited by 4
- Submonoid.prod_le_iffproof · cited by 4
- Submonoid.eq_bot_iff_forallproof · cited by 3
- Algebra.QuasiFiniteAt.exists_basicOpen_eq_singletonproof · cited by 2
- circleAverage_log_norm_sub_const₀proof · cited by 1
- Submonoid.nontrivial_iff_exists_ne_oneproof · cited by 1
- Ideal.isPrime_of_maximally_disjointproof · cited by 1
- IsLocalization.isRegular_mk'proof · cited by 1