Theorems · Definition · category theory
AddSemigrp.carrier
AddSemigrp → Type u
The underlying type.
- Defined in
- Mathlib.Algebra.Category.Semigrp.Basic
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddSemigrpstatement and proof · cited by 25
Cited by30
Results whose statement or proof uses this declaration.
- AddSemigrp.Hom.homstatement · cited by 9
- AddMonCat.adjoinZeroproof · cited by 2
- AddSemigrp.Hom.extstatement and proof · cited by 2
- AddSemigrp.Hom.hom'statement · cited by 2
- AddSemigrp.extstatement and proof · cited by 1
- AddSemigrp.hom_extstatement · cited by 1
- AddMonCat.adjoinZeroAdjstatement · cited by 0
- AddMonCat.adjoinZero_mapstatement · cited by 0
- AddMonCat.adjoinZero_obj_coestatement · cited by 0
- CategoryTheory.Iso.addSemigrpIsoToAddEquivstatement · cited by 0
- AddSemigrp.addEquiv_coe_eqstatement · cited by 0
- AddSemigrp.coe_compstatement · cited by 0