Commit 2025-09-15 20:56 847721aa

View on Github →

feat: group objects form a cartesian-monoidal category (#29166) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

added theorem GrpObj.tensorObj.Grp_.associator_hom_hom

added theorem GrpObj.tensorObj.Grp_.associator_inv_hom

added theorem GrpObj.tensorObj.Grp_.braiding_hom_hom

added theorem GrpObj.tensorObj.Grp_.braiding_inv_hom

added theorem GrpObj.tensorObj.Grp_.fst_hom

added theorem GrpObj.tensorObj.Grp_.leftUnitor_hom_hom

added theorem GrpObj.tensorObj.Grp_.leftUnitor_inv_hom

added theorem GrpObj.tensorObj.Grp_.lift_hom

added theorem GrpObj.tensorObj.Grp_.rightUnitor_hom_hom

added theorem GrpObj.tensorObj.Grp_.rightUnitor_inv_hom

added theorem GrpObj.tensorObj.Grp_.snd_hom

added theorem GrpObj.tensorObj.Grp_.tensorObj_mul

added theorem GrpObj.tensorObj.Grp_.tensorObj_one

added theorem GrpObj.tensorObj.Grp_.tensorUnit_X

added theorem GrpObj.tensorObj.Grp_.tensorUnit_mul

added theorem GrpObj.tensorObj.Grp_.tensorUnit_one

added theorem GrpObj.tensorObj.Grp_.whiskerLeft_hom

added theorem GrpObj.tensorObj.Grp_.whiskerRight_hom