Theorems · Theorem · category theory
CoalgCat.ofComonObjCoalgebraStruct_comul
∀ {R : Type u} [inst : CommRing R] (X : ModuleCat R) [inst_1 : CategoryTheory.ComonObj X],
CoalgebraStruct.comul = ModuleCat.Hom.hom CategoryTheory.ComonObj.comul- Cited by
- 4 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- LinearMapstatement · cited by 10,215
- CategoryTheory.MonoidalCategoryStruct.tensorObjstatement · cited by 3,106
- ModuleCatstatement and proof · cited by 1,429
- ModuleCat.carrierstatement · cited by 997
- ModuleCat.Hom.homstatement · cited by 341
- CoalgebraStruct.comulstatement and proof · cited by 118
- CategoryTheory.ComonObj.comulstatement · cited by 71
- CategoryTheory.ComonObjstatement and proof · cited by 48
Cited by4
Results whose statement or proof uses this declaration.
- CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_leftproof · cited by 0
- CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_rightproof · cited by 0
- CoalgCat.MonoidalCategoryAux.tensorObj_comulproof · cited by 0
- CoalgCat.MonoidalCategoryAux.comul_tensorObjproof · cited by 0