Mathlib Map

Theorems · Definition · group theory

MonoidHom.compHom

{M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      [inst : MulOneClass M] → [inst_1 : CommMonoid N] → [inst_2 : CommMonoid P] → (N →* P) →* (M →* N) →* M →* P

Composition of monoid morphisms (MonoidHom.comp) as a monoid morphism. Note that unlike MonoidHom.comp_hom' this requires commutativity of N.

Defined in
Mathlib.Algebra.Group.Hom.Instances
Cited by
5 results in Mathlib
Foundations
Depth 21 from the axioms · uses propext, Quot.sound
Assumes
MulOneClassCommMonoidCommMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CommMonCat.coyoneda · cited by 5CommMonCat.coyonedaCommGrpCat.coyoneda · cited by 5CommGrpCat.coyonedaMonoidHom.compr₂ · cited by 1MonoidHom.compr₂CommMonCat.coyoneda_map_app · cited by 0CommMonCat.coyoneda_map_a…CommMonCat.coyoneda_obj_map · cited by 0CommMonCat.coyoneda_obj_m…CommGrpCat.coyoneda_map_app · cited by 0CommGrpCat.coyoneda_map_a…CommGrpCat.coyoneda_obj_map · cited by 0CommGrpCat.coyoneda_obj_m…MonoidHom.compHom_apply_apply · cited by 0MonoidHom.compHom_apply_a…MonoidHom · cited by 3629MonoidHomCommMonoid · cited by 2264CommMonoidMulOneClass · cited by 1018MulOneClassMonoidHom.comp · cited by 469MonoidHom.compMonoidHom.comp_mul · cited by 0MonoidHom.comp_mulMonoidHom.compHomCITED BYCITES

Cites5

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

Cited by8

Results whose statement or proof uses this declaration.