Mathlib Map

Theorems · Definition · category theory

HopfAlgCat.carrier

{R : Type u} → [inst : CommRing R] → HopfAlgCat R → Type v

The underlying type.

Defined in
Mathlib.Algebra.Category.HopfAlgCat.Basic
Cited by
28 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

HopfAlgCat.Hom.toBialgHom · cited by 6Hom.toBialgHomHopfAlgCat.Hom.toBialgHom' · cited by 6Hom.toBialgHom'CategoryTheory.Iso.toHopfAlgEquiv · cited by 4Iso.toHopfAlgEquivHopfAlgCat.Hom.ext · cited by 2Hom.extHopfAlgCat.MonoidalCategory.inducingFunctorData · cited by 2MonoidalCategory.inducing…HopfAlgCat.hom_ext · cited by 1HopfAlgCat.hom_extHopfAlgCat.Hom.mk.inj · cited by 1mk.injHopfAlgCat.Hom.mk.noConfusion · cited by 1mk.noConfusionHopfAlgCat.associator_def · cited by 0HopfAlgCat.associator_defHopfAlgCat.forget₂_bialgebra_map · cited by 0HopfAlgCat.forget₂_bialge…HopfAlgCat.forget₂_bialgebra_obj · cited by 0HopfAlgCat.forget₂_bialge…CategoryTheory.Iso.toHopfAlgEquiv_refl · cited by 0Iso.toHopfAlgEquiv_reflHopfAlgCat.hom_ext_iff · cited by 0HopfAlgCat.hom_ext_iffCategoryTheory.Iso.toHopfAlgEquiv_symm · cited by 0Iso.toHopfAlgEquiv_symmCategoryTheory.Iso.toHopfAlgEquiv_toBialgHom · cited by 0Iso.toHopfAlgEquiv_toBial…CommRing · cited by 17173CommRingHopfAlgCat · cited by 31HopfAlgCatHopfAlgCat.carrierCITED BYCITES

Cites2

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

  • CommRingstatement and proof · cited by 17,173
  • HopfAlgCatstatement and proof · cited by 31

Cited by37

Results whose statement or proof uses this declaration.