Mathlib Map

Theorems · Inductive type · category theory

AddMonCat

Type (u + 1)

The category of additive monoids and monoid morphisms.

Defined in
Mathlib.Algebra.Category.MonCat.Basic
Cited by
71 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddMonCat.carrier · cited by 60AddMonCat.carrierAddMonCat.Hom.hom · cited by 21Hom.homAddMonCat.ofHom · cited by 17AddMonCat.ofHomAddMonCat.of · cited by 16AddMonCat.ofCategoryTheory.yonedaAddMonObj · cited by 12CategoryTheory.yonedaAddM…CategoryTheory.yonedaAddMon · cited by 8CategoryTheory.yonedaAddM…AddMonCat.FilteredColimits.M · cited by 8FilteredColimits.MAddMonCat.FilteredColimits.M.mk · cited by 6M.mkAddMonCat.equivalence · cited by 6AddMonCat.equivalenceCategoryTheory.AddMonObj.ofRepresentableBy · cited by 6AddMonObj.ofRepresentable…AddGrpCat.FilteredColimits.G · cited by 6FilteredColimits.GAddMonCat.FilteredColimits.M.mk_eq · cited by 5M.mk_eqCategoryTheory.AddGrpObj.ofRepresentableBy · cited by 4AddGrpObj.ofRepresentable…CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy · cited by 3CategoryTheory.yonedaAddM…AddMonCat.FilteredColimits.colimit_add_mk_eq · cited by 3FilteredColimits.colimit_…AddMonCatCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by134

Results whose statement or proof uses this declaration.