Commit 2025-02-12 14:33 37ae3a8c

View on Github →

feat(Algebra/Category): chosen finite products for group-like categories (#21737)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/Biproducts.lean

Created Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean

added theorem AddCommGrp.tensorObj_eq

added theorem AddCommGrp.μ_forget_apply

added def AddGrp.binaryProductLimitCone

added theorem AddGrp.tensorObj_eq

added theorem AddGrp.μ_forget_apply

added def CommGrp.binaryProductLimitCone

added theorem CommGrp.tensorObj_eq

added theorem CommGrp.μ_forget_apply

added def Grp.binaryProductLimitCone

added theorem Grp.tensorObj_eq

added theorem Grp.μ_forget_apply

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

modified theorem CategoryTheory.Functor.Monoidal.δ_fst

modified theorem CategoryTheory.Functor.Monoidal.δ_snd

modified theorem CategoryTheory.Functor.Monoidal.μ_fst

modified theorem CategoryTheory.Functor.Monoidal.μ_snd