CommMon_

Statistics

Metric	Count
Definitions	0
Theorems `ofRepresentableBy`	1
Total	1

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`

---