Commit 2023-05-19 16:59 afc77211

View on Github →

Port/category_theory.monoidal.of_chosen_finite_products.basic (#4115)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean

added def CategoryTheory.Limits.BinaryFan.assoc

added def CategoryTheory.Limits.BinaryFan.assocInv

added theorem CategoryTheory.Limits.BinaryFan.assocInv_fst

added theorem CategoryTheory.Limits.BinaryFan.assocInv_snd

added theorem CategoryTheory.Limits.BinaryFan.assoc_fst

added theorem CategoryTheory.Limits.BinaryFan.assoc_snd

added def CategoryTheory.Limits.BinaryFan.associator

added def CategoryTheory.Limits.BinaryFan.associatorOfLimitCone

added def CategoryTheory.Limits.BinaryFan.braiding

added def CategoryTheory.Limits.BinaryFan.leftUnitor

added def CategoryTheory.Limits.BinaryFan.rightUnitor

added def CategoryTheory.Limits.BinaryFan.swap

added theorem CategoryTheory.Limits.BinaryFan.swap_fst

added theorem CategoryTheory.Limits.BinaryFan.swap_snd

added theorem CategoryTheory.Limits.HasBinaryProduct.swap

added def CategoryTheory.Limits.IsLimit.assoc

added def CategoryTheory.Limits.IsLimit.swapBinaryFan

added def CategoryTheory.MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.associator_naturality

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.leftUnitor_naturality

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.pentagon

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.rightUnitor_naturality

added def CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom

added def CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.tensor_comp

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.tensor_id

added theorem CategoryTheory.MonoidalOfChosenFiniteProducts.triangle

added def CategoryTheory.monoidalOfChosenFiniteProducts