Theorems · Definition · group theory

AddHom.codRestrict

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

Restriction of an AddSemigroup hom to an AddSubsemigroup 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: Add Add SetLike AddMemClass

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
AddHomstatement and proof · cited by 294
AddMemClassstatement and proof · cited by 17

Cited by3

Results whose statement or proof uses this declaration.

AddHom.srangeRestrictproof · cited by 3
AddSubsemigroup.inclusionproof · cited by 0
AddHom.codRestrict_apply_coestatement and proof · cited by 0