Cartesian

📁 Source: Mathlib/CategoryTheory/Distributive/Cartesian.lean

Statistics

Metric	Count
Definitions IsCartesianDistributive	1
Theorems monoCoprod, of_isMonoidalLeftDistrib	2
Total	3

CategoryTheory

Definitions

Name	Category	Theorems
IsCartesianDistributive 📖	MathDef	1 math math: IsCartesianDistributive.of_isMonoidalLeftDistrib

CategoryTheory.IsCartesianDistributive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monoCoprod 📖	mathematical	—	CategoryTheory.Limits.MonoCoprod	—	CategoryTheory.Limits.MonoCoprod.mk' CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.SplitMono.mono CategoryTheory.IsMonoidalDistrib.toIsMonoidalLeftDistrib CategoryTheory.CartesianMonoidalCategory.comp_lift CategoryTheory.Category.comp_id CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.cancel_mono CategoryTheory.CartesianMonoidalCategory.lift_whiskerLeft CategoryTheory.CartesianMonoidalCategory.lift_snd CategoryTheory.eq_whisker
of_isMonoidalLeftDistrib 📖	mathematical	—	CategoryTheory.IsCartesianDistributive	—	CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib CategoryTheory.CartesianMonoidalCategory.instNonemptyBraidedCategory

---

← Back to Index