Mathlib Map

Theorems · Definition · category theory

CommHopfAlgCat.X

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

The underlying type.

Defined in
Mathlib.Algebra.Category.CommHopfAlgCat
Cited by
30 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.

CommHopfAlgCat.Hom.hom · cited by 12Hom.homcommHopfAlgCatEquivCogrpCommAlgCat · cited by 6commHopfAlgCatEquivCogrpC…CommHopfAlgCat.ofIso · cited by 3CommHopfAlgCat.ofIsoCommHopfAlgCat.Hom.ext · cited by 2Hom.extCommHopfAlgCat.Hom.hom' · cited by 2Hom.hom'CommHopfAlgCat.ofIsoSelf · cited by 2CommHopfAlgCat.ofIsoSelfCommHopfAlgCat.hom_ext · cited by 1CommHopfAlgCat.hom_extCommHopfAlgCat.Hom.mk.inj · cited by 1mk.injCommHopfAlgCat.Hom.mk.noConfusion · cited by 1mk.noConfusionCommHopfAlgCat.Hom.noConfusionType · cited by 0Hom.noConfusionTypeCommHopfAlgCat.coe_of · cited by 0CommHopfAlgCat.coe_ofCommHopfAlgCat.comp_apply · cited by 0CommHopfAlgCat.comp_applyCommHopfAlgCat.forget_obj · cited by 0CommHopfAlgCat.forget_objCommHopfAlgCat.forget₂_commBialgCat_map · cited by 0CommHopfAlgCat.forget₂_co…CommHopfAlgCat.forget₂_commBialgCat_obj · cited by 0CommHopfAlgCat.forget₂_co…CommRing · cited by 17173CommRingCommHopfAlgCat · cited by 38CommHopfAlgCatCommHopfAlgCat.XCITED BYCITES

Cites2

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

Cited by41

Results whose statement or proof uses this declaration.