Mathlib Map

Theorems · Definition · category theory

MonCat.of

(M : Type u) → [Monoid M] → MonCat

Construct a bundled MonCat from the underlying type and typeclass.

Defined in
Mathlib.Algebra.Category.MonCat.Basic
Cited by
22 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MonCat.ofHom · cited by 24MonCat.ofHomCategoryTheory.yonedaMonObj · cited by 12CategoryTheory.yonedaMonO…CategoryTheory.SubmonoidFunctor.toFunctor · cited by 8SubmonoidFunctor.toFunctorMonCat.shrinkFunctor · cited by 6MonCat.shrinkFunctorAddMonCat.equivalence · cited by 6AddMonCat.equivalenceMonCat.uliftFunctor · cited by 2MonCat.uliftFunctorMonCat.Colimits.colimit · cited by 2Colimits.colimitMulEquiv.toMonCatIso · cited by 2MulEquiv.toMonCatIsoMonCat.adjoinOne · cited by 2MonCat.adjoinOneMonCat.FilteredColimits.colimit · cited by 1FilteredColimits.colimitMonCat.hom_ofHom · cited by 0MonCat.hom_ofHomCategoryTheory.SubmonoidFunctor.toFunctor_map · cited by 0SubmonoidFunctor.toFuncto…CategoryTheory.SubmonoidFunctor.toFunctor_obj · cited by 0SubmonoidFunctor.toFuncto…MonCat.mul_of · cited by 0MonCat.mul_ofMonCat.ofHom_apply · cited by 0MonCat.ofHom_applyMonoid · cited by 3887MonoidMonCat · cited by 127MonCatMonCat.ofCITED BYCITES

Cites2

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

  • Monoidstatement and proof · cited by 3,887
  • MonCatstatement · cited by 127

Cited by37

Results whose statement or proof uses this declaration.