Theorems · Definition · group theory
Submonoid.subtype
{M : Type u_4} → [inst : MulOneClass M] → (S : Submonoid M) → ↥S →* MThe natural monoid hom from a submonoid of monoid M to M.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- 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.
- MonoidHomstatement · cited by 3,629
- Submonoidstatement and proof · cited by 3,086
- MulOneClassstatement and proof · cited by 1,018
Cited by36
Results whose statement or proof uses this declaration.
- Subring.subtypeproof · cited by 22
- Subfield.subtypeproof · cited by 16
- Subsemiring.subtypeproof · cited by 11
- Submonoid.inclusionproof · cited by 6
- unitsNonZeroDivisorsEquivproof · cited by 6
- orderOf_submonoidproof · cited by 5
- CategoryTheory.SubmonoidFunctor.ιproof · cited by 4
- Submonoid.coe_finsetProdproof · cited by 4
- IsLocalization.exist_integer_multiplesproof · cited by 4
- Submonoid.mrange_subtypestatement and proof · cited by 4
- unitSphereToUnitsproof · cited by 2
- unitsCenterToCenterUnitsproof · cited by 2