Commit 2025-02-15 11:19 d410bf63

View on Github →

feat(CategoryTheory): commutative group objects (#21508)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

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 theorem CommGrp_.mkIso_hom_hom

added theorem CommGrp_.mkIso_inv_hom

added def CommGrp_.trivial

added structure CommGrp_