Mathlib Map

Theorems · Definition · category theory

BialgCat.carrier

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

The underlying type.

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

BialgCat.Hom.toBialgHom · cited by 7Hom.toBialgHomBialgCat.Hom.toBialgHom' · cited by 6Hom.toBialgHom'CategoryTheory.Iso.toBialgEquiv · cited by 4Iso.toBialgEquivBialgCat.Hom.ext · cited by 2Hom.extBialgCat.MonoidalCategory.inducingFunctorData · cited by 2MonoidalCategory.inducing…HopfAlgCat.MonoidalCategory.inducingFunctorData · cited by 2MonoidalCategory.inducing…BialgCat.hom_ext · cited by 1BialgCat.hom_extBialgCat.Hom.mk.inj · cited by 1mk.injBialgCat.Hom.mk.noConfusion · cited by 1mk.noConfusionHopfAlgCat.MonoidalCategory.inducingFunctorData_μIso · cited by 0MonoidalCategory.inducing…CategoryTheory.Iso.toBialgEquiv_refl · cited by 0Iso.toBialgEquiv_reflCategoryTheory.Iso.toBialgEquiv_symm · cited by 0Iso.toBialgEquiv_symmCategoryTheory.Iso.toBialgEquiv_toBialgHom · cited by 0Iso.toBialgEquiv_toBialgH…CategoryTheory.Iso.toBialgEquiv_trans · cited by 0Iso.toBialgEquiv_transHopfAlgCat.forget₂_bialgebra_map · cited by 0HopfAlgCat.forget₂_bialge…CommRing · cited by 17173CommRingBialgCat · cited by 40BialgCatBialgCat.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
  • BialgCatstatement and proof · cited by 40

Cited by44

Results whose statement or proof uses this declaration.