Theorems · Definition · group theory
AddSubmonoid.subtype
{M : Type u_4} → [inst : AddZeroClass M] → (S : AddSubmonoid M) → ↥S →+ MThe natural monoid hom from an AddSubmonoid of AddMonoid M to M.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext
- Assumes
- AddZeroClass
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.
- AddMonoidHomstatement · cited by 3,230
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement and proof · cited by 1,178
Cited by32
Results whose statement or proof uses this declaration.
- Subsemiring.subtypeproof · cited by 11
- AddSubmonoid.inclusionproof · cited by 7
- AddSubmonoid.coe_finsetSumproof · cited by 5
- AddSubmonoid.mrange_subtypestatement and proof · cited by 4
- AddMonoid.fg_iff_addSubmonoid_fgproof · cited by 3
- AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHomstatement and proof · cited by 2
- addUnitsCenterToCenterAddUnitsproof · cited by 2
- IsSemilinearSet.interproof · cited by 2
- AddEquiv.ofLeftInverse'proof · cited by 2
- AddSubmonoid.mem_iSup_iff_exists_dfinsuppstatement · cited by 1
- AddSubmonoid.coe_subtypestatement · cited by 1
- AddMonoidHom.domRestrict_mkerstatement · cited by 1