MonoidHom.restrictHom

Deprecated since 2026-07-19Use MonoidHom.domRestrictHom instead.

{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

Alias of MonoidHom.domRestrictHom. A version of MonoidHom.domRestrict as a homomorphism.

Defined in: Mathlib.Algebra.Group.Submonoid.Operations
Cited by: 0 results in Mathlib
Foundations: Depth 22 from the axioms · uses propext, Quot.sound
Assumes: MulOneClass SetLike SubmonoidClass CommMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

MonoidHomstatement · cited by 3,629
CommMonoidstatement · cited by 2,264
SetLikestatement · cited by 1,084
MulOneClassstatement · cited by 1,018
SubmonoidClassstatement · cited by 60
MonoidHom.domRestrictHomproof · cited by 12

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.