Mathlib Map

Theorems · Inductive type · category theory

AddCommMonCat

Type (u + 1)

The category of additive commutative monoids and monoid morphisms.

Defined in
Mathlib.Algebra.Category.MonCat.Basic
Cited by
50 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.

AddCommMonCat.carrier · cited by 41AddCommMonCat.carrierAddCommMonCat.of · cited by 20AddCommMonCat.ofAddCommMonCat.ofHom · cited by 18AddCommMonCat.ofHomAddCommMonCat.Hom.hom · cited by 17Hom.homAddCommMonCat.equivalence · cited by 6AddCommMonCat.equivalenceAddCommMonCat.coyoneda · cited by 5AddCommMonCat.coyonedaAddCommMonCat.coyonedaType · cited by 3AddCommMonCat.coyonedaTypeSemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom · cited by 2colimitCoconeIsColimit.de…AddEquiv.toAddCommMonCatIso · cited by 2AddEquiv.toAddCommMonCatI…AddCommMonCat.Hom · cited by 2AddCommMonCat.HomAddCommMonCat.Hom.ext · cited by 2Hom.extAddCommMonCat.coyonedaForget · cited by 2AddCommMonCat.coyonedaFor…AddCommMonCat.free · cited by 2AddCommMonCat.freeAddCommMonCat.uliftFunctor · cited by 2AddCommMonCat.uliftFunctorAddCommMonCat.Hom.hom' · cited by 2Hom.hom'AddCommMonCatCITED 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 by92

Results whose statement or proof uses this declaration.