Def AddGrp.binaryProductLimitCone

Modification history

2025-02-12 14:33

Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean

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

Added AddGrp.binaryProductLimitCone View on Github →