Theorems · Definition · group theory

MonoidHom.domRestrictHom

{M : Type u_1} →
  [inst : MulOneClass M] →
    {S : Type u_5} →
      [inst_1 : SetLike S M] →
        [inst_2 : SubmonoidClass S M] → (M' : S) → (A : Type u_6) → [inst_3 : CommMonoid A] → (M →* A) →* ↥M' →* A

A version of MonoidHom.domRestrict as a homomorphism.

Defined in

Mathlib.Algebra.Group.Submonoid.Operations

Cited by

12 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

MulOneClassSetLikeSubmonoidClassCommMonoid