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