Theorems · Inductive type · group theory
Submonoid
(M : Type u_3) → [MulOneClass M] → Type u_3
A submonoid of a monoid M is a subset containing 1 and closed under multiplication.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 3,086 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- MulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulOneClassstatement · cited by 1,018
Cited by3,629
Results whose statement or proof uses this declaration.
- nonZeroDivisorsstatement · cited by 895
- IsLocalizationstatement · cited by 636
- Ideal.primeComplstatement · cited by 462
- FractionalIdealstatement and proof · cited by 423
- Submonoid.powersstatement · cited by 408
- Subgroup.mapproof · cited by 301
- Localizationstatement and proof · cited by 270
- MulAction.stabilizerproof · cited by 254
- IsLocalizedModulestatement · cited by 220
- IsLocalization.mk'statement and proof · cited by 218
- MonoidHom.kerproof · cited by 212
- unitarystatement · cited by 207
Showing the 200 most cited of 3,629.