Mathlib Map

Theorems · Inductive type

MonoidHom.CompTriple

{M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : Monoid M] → [inst_1 : Monoid N] → [inst_2 : Monoid P] → (M →* N) → (N →* P) → outParam (M →* P) → Prop

Class of composing triples

Defined in
Mathlib.Algebra.Group.Hom.CompTypeclasses
Cited by
14 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
MonoidMonoidMonoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NonUnitalAlgHom.comp · cited by 21NonUnitalAlgHom.compDistribMulActionHom.comp · cited by 13DistribMulActionHom.compMonoidHom.CompTriple.comp_eq · cited by 4CompTriple.comp_eqMulDistribMulActionHom.comp · cited by 4MulDistribMulActionHom.co…MulSemiringActionHom.comp · cited by 3MulSemiringActionHom.compDistribMulActionHom.comp_apply · cited by 2DistribMulActionHom.comp_…MulDistribMulActionHom.comp_apply · cited by 2MulDistribMulActionHom.co…MulSemiringActionHom.comp_apply · cited by 2MulSemiringActionHom.comp…MonoidHom.CompTriple.casesOn · cited by 1CompTriple.casesOnMonoidHom.CompTriple.comp · cited by 0CompTriple.compMonoidHom.CompTriple.comp_apply · cited by 0CompTriple.comp_applyMonoidHom.CompTriple.comp_assoc · cited by 0CompTriple.comp_assocMonoidHom.CompTriple.comp_inv · cited by 0CompTriple.comp_invDistribMulActionHom.comp_assoc · cited by 0DistribMulActionHom.comp_…MonoidHom.CompTriple.recOn · cited by 0CompTriple.recOnMonoid · cited by 3887MonoidMonoidHom · cited by 3629MonoidHomMonoidHom.CompTripleCITED BYCITES

Cites2

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

Cited by20

Results whose statement or proof uses this declaration.