Mathlib Map

Theorems · Inductive type · category theory

Semigrp

Type (u + 1)

The category of semigroups and semigroup morphisms.

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

Semigrp.carrier · cited by 21Semigrp.carrierSemigrp.Hom.hom · cited by 9Hom.homSemigrp.of · cited by 9Semigrp.ofSemigrp.ofHom · cited by 8Semigrp.ofHomSemigrp.Hom.ext · cited by 2Hom.extSemigrp.Hom.hom' · cited by 2Hom.hom'MonCat.adjoinOne · cited by 2MonCat.adjoinOneMulEquiv.toSemigrpIso · cited by 2MulEquiv.toSemigrpIsoSemigrp.Hom · cited by 2Semigrp.HomSemigrp.mk.inj · cited by 1mk.injSemigrp.mk.noConfusion · cited by 1mk.noConfusionSemigrp.ext · cited by 1Semigrp.extSemigrp.hom_ext · cited by 1Semigrp.hom_extSemigrp.Hom.casesOn · cited by 0Hom.casesOnSemigrp.Hom.ctorIdx · cited by 0Hom.ctorIdxSemigrpCITED 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 by48

Results whose statement or proof uses this declaration.