Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-02-14 06:25
e6816f7d
View on Github →
feat port/CategoryTheory.Products.Basic (
#2211
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Products/Basic.lean
added
def
CategoryTheory.Functor.constCompEvaluationObj
added
def
CategoryTheory.Functor.diag
added
theorem
CategoryTheory.Functor.diag_map
added
theorem
CategoryTheory.Functor.diag_obj
added
def
CategoryTheory.Functor.prod'
added
def
CategoryTheory.Functor.prod'CompFst
added
def
CategoryTheory.Functor.prod'CompSnd
added
def
CategoryTheory.Functor.prod
added
def
CategoryTheory.Iso.prod
added
def
CategoryTheory.NatTrans.prod
added
def
CategoryTheory.Prod.braiding
added
def
CategoryTheory.Prod.fst
added
def
CategoryTheory.Prod.sectl
added
def
CategoryTheory.Prod.sectr
added
def
CategoryTheory.Prod.snd
added
def
CategoryTheory.Prod.swap
added
def
CategoryTheory.Prod.symmetry
added
def
CategoryTheory.evaluation
added
def
CategoryTheory.evaluationUncurried
added
def
CategoryTheory.flipCompEvaluation
added
def
CategoryTheory.functorProdFunctorEquiv
added
def
CategoryTheory.functorProdFunctorEquivCounitIso
added
def
CategoryTheory.functorProdFunctorEquivUnitIso
added
def
CategoryTheory.functorProdToProdFunctor
added
theorem
CategoryTheory.isIso_prod_iff
added
def
CategoryTheory.prod.etaIso
added
def
CategoryTheory.prodFunctorToFunctorProd
added
theorem
CategoryTheory.prod_comp
added
theorem
CategoryTheory.prod_id