CommMon_

📁 Source: Mathlib/CategoryTheory/Monoidal/Cartesian/CommMon_.lean

Statistics

Metric	Count
Definitions	0
Theorems ofRepresentableBy, ofRepresentableBy	2
Total	2

CategoryTheory.IsCommMon

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofRepresentableBy 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.ofRepresentableBy CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommMonCat CommMonCat.instCategory MonCat MonCat.instCategory CategoryTheory.forget₂ MonoidHom CommMonCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid CommMonCat.str MonoidHom.instFunLike CommMonCat.instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier CommMonCat.hasForgetToMonCat	—	CategoryTheory.IsCommMonObj.ofRepresentableBy

CategoryTheory.IsCommMonObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofRepresentableBy 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.MonObj.ofRepresentableBy CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CommMonCat CommMonCat.instCategory MonCat MonCat.instCategory CategoryTheory.forget₂ MonoidHom CommMonCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid CommMonCat.str MonoidHom.instFunLike CommMonCat.instConcreteCategoryMonoidHomCarrier MonCat.carrier MonCat.str MonCat.instConcreteCategoryMonoidHomCarrier CommMonCat.hasForgetToMonCat	—	Equiv.apply_eq_iff_eq CategoryTheory.Functor.RepresentableBy.homEquiv_comp Equiv.apply_symm_apply map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass CategoryTheory.CartesianMonoidalCategory.braiding_hom_fst CategoryTheory.CartesianMonoidalCategory.braiding_hom_snd mul_comm

---

← Back to Index