Commit 2023-05-26 10:07 e2689971

View on Github →

feat: port Algebra.Category.Module.Biproducts (#4386)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

added def ModuleCat.HasLimit.lift

added def ModuleCat.HasLimit.productLimitCone

added def ModuleCat.binaryProductLimitCone

added theorem ModuleCat.binaryProductLimitCone_cone_π_app_left

added theorem ModuleCat.binaryProductLimitCone_cone_π_app_right

added theorem ModuleCat.biprodIsoProd_inv_comp_fst

added theorem ModuleCat.biprodIsoProd_inv_comp_snd

added theorem ModuleCat.biproductIsoPi_inv_comp_π