Mathlib Map

Theorems · Definition · group theory

MulMemClass.subtype

{M : Type u_1} →
  {A : Type u_3} → [inst : Mul M] → [inst_1 : SetLike A M] → [hA : MulMemClass A M] → (S' : A) → ↥S' →ₙ* M

The natural semigroup hom from a subsemigroup of semigroup M to M.

Defined in
Mathlib.Algebra.Group.Subsemigroup.Defs
Cited by
5 results in Mathlib
Foundations
Depth 9 from the axioms · uses no axioms
Assumes
MulSetLikeMulMemClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NonUnitalSubsemiringClass.subtype · cited by 5NonUnitalSubsemiringClass…MulEquiv.ofLeftInverse · cited by 2MulEquiv.ofLeftInverseMulHom.domRestrict · cited by 2MulHom.domRestrictSubsemigroup.inclusion · cited by 0Subsemigroup.inclusionMulMemClass.coe_subtype · cited by 0MulMemClass.coe_subtypeSubsemigroup.topEquiv_toMulHom · cited by 0Subsemigroup.topEquiv_toM…MulMemClass.subtype_apply · cited by 0MulMemClass.subtype_applyMulMemClass.subtype_injective · cited by 0MulMemClass.subtype_injec…Subsemigroup.range_subtype · cited by 0Subsemigroup.range_subtypeSetLike · cited by 1084SetLikeMulHom · cited by 299MulHomMulMemClass · cited by 25MulMemClassMulMemClass.subtypeCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • SetLikestatement and proof · cited by 1,084
  • MulHomstatement · cited by 299
  • MulMemClassstatement and proof · cited by 25

Cited by9

Results whose statement or proof uses this declaration.