Commit 2025-10-16 01:23 5aecb234

View on Github →

chore: rename Grp_ to Grp (#30496) Zulip

Estimated changes

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

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

added def Grp.homMk

added theorem Grp.homMk_hom'

deleted def Grp_.homMk

deleted theorem Grp_.homMk_hom'

modified def yonedaGrp

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

modified theorem CategoryTheory.Functor.comp_mapCommGrp_mul

modified theorem CategoryTheory.Functor.comp_mapCommGrp_one

modified def CategoryTheory.Functor.mapCommGrp

modified def CategoryTheory.Functor.mapCommGrpIdIso

modified theorem CategoryTheory.Functor.mapCommGrp_id_one

modified theorem CategoryTheory.Functor.mapCommpGrp_id_mul

added theorem CommGrp.comp'

added theorem CommGrp.comp_hom

added def CommGrp.forget

added def CommGrp.forget₂CommMon

added theorem CommGrp.forget₂CommMon_comp_forget

added theorem CommGrp.forget₂CommMon_map_hom

added theorem CommGrp.forget₂CommMon_obj_mul

added theorem CommGrp.forget₂CommMon_obj_one

added def CommGrp.forget₂Grp

added theorem CommGrp.forget₂Grp_comp_forget

added theorem CommGrp.forget₂Grp_map_hom

added theorem CommGrp.forget₂Grp_obj_mul

added theorem CommGrp.forget₂Grp_obj_one

added def CommGrp.fullyFaithfulForget₂CommMon

added def CommGrp.fullyFaithfulForget₂Grp

added theorem CommGrp.hom_ext

added theorem CommGrp.id'

added theorem CommGrp.id_hom

added def CommGrp.mkIso'

added def CommGrp.toCommMon

added def CommGrp.toGrp

added def CommGrp.trivial

added structure CommGrp

deleted theorem CommGrp_.comp'

deleted theorem CommGrp_.comp_hom

deleted def CommGrp_.forget

deleted def CommGrp_.forget₂CommMon

deleted theorem CommGrp_.forget₂CommMon_comp_forget

deleted theorem CommGrp_.forget₂CommMon_map_hom

deleted theorem CommGrp_.forget₂CommMon_obj_mul

deleted theorem CommGrp_.forget₂CommMon_obj_one

deleted def CommGrp_.forget₂Grp_

deleted theorem CommGrp_.forget₂Grp_comp_forget

deleted theorem CommGrp_.forget₂Grp_map_hom

deleted theorem CommGrp_.forget₂Grp_obj_mul

deleted theorem CommGrp_.forget₂Grp_obj_one

deleted def CommGrp_.fullyFaithfulForget₂CommMon

deleted def CommGrp_.fullyFaithfulForget₂Grp_

deleted theorem CommGrp_.hom_ext

deleted theorem CommGrp_.id'

deleted theorem CommGrp_.id_hom

deleted def CommGrp_.mkIso'

deleted def CommGrp_.toCommMon

deleted def CommGrp_.toGrp_

deleted def CommGrp_.trivial

deleted structure CommGrp_

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

added theorem Grp.comp'

added theorem Grp.comp_hom

added theorem Grp.hom_ext

added theorem Grp.id'

added theorem Grp.id_hom

added def Grp.toMon

added def Grp.trivial

added structure Grp

modified def GrpObj.tensorObj.CategoryTheory.Equivalence.mapGrp

modified theorem GrpObj.tensorObj.CategoryTheory.Functor.comp_mapGrp_mul

modified theorem GrpObj.tensorObj.CategoryTheory.Functor.comp_mapGrp_one

modified theorem GrpObj.tensorObj.CategoryTheory.Functor.essImage_mapGrp

modified def GrpObj.tensorObj.CategoryTheory.Functor.mapGrp

modified def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpIdIso

modified theorem GrpObj.tensorObj.CategoryTheory.Functor.mapGrp_id_mul

modified theorem GrpObj.tensorObj.CategoryTheory.Functor.mapGrp_id_one

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 def GrpObj.tensorObj.Grp.forget

added def GrpObj.tensorObj.Grp.forget₂Mon

added theorem GrpObj.tensorObj.Grp.forget₂Mon_comp_forget

added theorem GrpObj.tensorObj.Grp.forget₂Mon_map_hom

added theorem GrpObj.tensorObj.Grp.forget₂Mon_obj_mul

added theorem GrpObj.tensorObj.Grp.forget₂Mon_obj_one

added theorem GrpObj.tensorObj.Grp.fst_hom

added def GrpObj.tensorObj.Grp.fullyFaithfulForget₂Mon

added theorem GrpObj.tensorObj.Grp.leftUnitor_hom_hom

added theorem GrpObj.tensorObj.Grp.leftUnitor_inv_hom

added theorem GrpObj.tensorObj.Grp.lift_hom

added def GrpObj.tensorObj.Grp.mkIso'

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

deleted theorem GrpObj.tensorObj.Grp_.associator_hom_hom

deleted theorem GrpObj.tensorObj.Grp_.associator_inv_hom

deleted theorem GrpObj.tensorObj.Grp_.braiding_hom_hom

deleted theorem GrpObj.tensorObj.Grp_.braiding_inv_hom

deleted def GrpObj.tensorObj.Grp_.forget

deleted def GrpObj.tensorObj.Grp_.forget₂Mon

deleted theorem GrpObj.tensorObj.Grp_.forget₂Mon_comp_forget

deleted theorem GrpObj.tensorObj.Grp_.forget₂Mon_map_hom

deleted theorem GrpObj.tensorObj.Grp_.forget₂Mon_obj_mul

deleted theorem GrpObj.tensorObj.Grp_.forget₂Mon_obj_one

deleted theorem GrpObj.tensorObj.Grp_.fst_hom

deleted def GrpObj.tensorObj.Grp_.fullyFaithfulForget₂Mon

deleted theorem GrpObj.tensorObj.Grp_.leftUnitor_hom_hom

deleted theorem GrpObj.tensorObj.Grp_.leftUnitor_inv_hom

deleted theorem GrpObj.tensorObj.Grp_.lift_hom

deleted def GrpObj.tensorObj.Grp_.mkIso'

deleted theorem GrpObj.tensorObj.Grp_.rightUnitor_hom_hom

deleted theorem GrpObj.tensorObj.Grp_.rightUnitor_inv_hom

deleted theorem GrpObj.tensorObj.Grp_.snd_hom

deleted theorem GrpObj.tensorObj.Grp_.tensorObj_mul

deleted theorem GrpObj.tensorObj.Grp_.tensorObj_one

deleted theorem GrpObj.tensorObj.Grp_.tensorUnit_X

deleted theorem GrpObj.tensorObj.Grp_.tensorUnit_mul

deleted theorem GrpObj.tensorObj.Grp_.tensorUnit_one

deleted theorem GrpObj.tensorObj.Grp_.whiskerLeft_hom

deleted theorem GrpObj.tensorObj.Grp_.whiskerRight_hom

deleted theorem Grp_.comp'

deleted theorem Grp_.comp_hom

deleted theorem Grp_.hom_ext

deleted theorem Grp_.id'

deleted theorem Grp_.id_hom

deleted def Grp_.toMon

deleted def Grp_.trivial

deleted structure Grp_

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean

Modified Mathlib/CategoryTheory/Preadditive/CommGrp_.lean

modified def CategoryTheory.Preadditive.commGrpEquivalence

modified def CategoryTheory.Preadditive.commGrpEquivalenceAux

modified def CategoryTheory.Preadditive.toCommGrp