Commit 2023-05-27 13:11 ba4e1ad1

View on Github →

feat: port Algebra.Category.GroupCat.Biproducts (#4411)

Estimated changes

Modified Mathlib.lean

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

added def AddCommGroupCat.HasLimit.lift

added def AddCommGroupCat.HasLimit.productLimitCone

added def AddCommGroupCat.binaryProductLimitCone

added theorem AddCommGroupCat.binaryProductLimitCone_cone_π_app_left

added theorem AddCommGroupCat.binaryProductLimitCone_cone_π_app_right

added theorem AddCommGroupCat.biprodIsoProd_inv_comp_fst

added theorem AddCommGroupCat.biprodIsoProd_inv_comp_snd

added theorem AddCommGroupCat.biproductIsoPi_inv_comp_π