Theorems · Definition · group theory

MulHom.codRestrict

{M : Type u_1} →
  {N : Type u_2} →
    {σ : Type u_4} →
      [inst : Mul M] →
        [inst_1 : Mul N] →
          [inst_2 : SetLike σ N] →
            [inst_3 : MulMemClass σ N] → (f : M →ₙ* N) → (S : σ) → (∀ (x : M), f x ∈ S) → M →ₙ* ↥S

Restriction of a semigroup hom to a subsemigroup of the codomain.

Defined in: Mathlib.Algebra.Group.Subsemigroup.Operations
Cited by: 1 results in Mathlib
Foundations: Depth 11 from the axioms · uses no axioms
Assumes: Mul Mul SetLike MulMemClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites4

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

DFunLike.coestatement and proof · cited by 62,936
SetLikestatement and proof · cited by 1,084
MulHomstatement and proof · cited by 299
MulMemClassstatement and proof · cited by 25

Cited by3

Results whose statement or proof uses this declaration.

MulHom.srangeRestrictproof · cited by 3
Subsemigroup.inclusionproof · cited by 0
MulHom.codRestrict_apply_coestatement and proof · cited by 0