Commit 2025-10-30 04:20 88367e02

View on Github →

chore(CategoryTheory): namespace Mon, Grp, etc... (#30786) After this is done, we can finally rename Mod_ to Mod.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Bimon_.lean

deleted theorem Bimon.BimonObjAux_comul

deleted theorem Bimon.BimonObjAux_counit

deleted theorem Bimon.comp_hom'

deleted theorem Bimon.compatibility

deleted def Bimon.equivMonComon

deleted def Bimon.equivMonComonCounitIsoApp

deleted def Bimon.equivMonComonCounitIsoAppX

deleted def Bimon.equivMonComonCounitIsoAppXAux

deleted def Bimon.equivMonComonUnitIsoApp

deleted def Bimon.equivMonComonUnitIsoAppX

deleted def Bimon.equivMonComonUnitIsoAppXAux

deleted theorem Bimon.ext

deleted def Bimon.forget

deleted theorem Bimon.id_hom'

deleted def Bimon.mk'

deleted def Bimon.mk'X

deleted theorem Bimon.mul_counit

deleted def Bimon.ofMonComon

deleted def Bimon.ofMonComonObj

deleted def Bimon.ofMonComonObjX

deleted theorem Bimon.ofMonComonObjX_mul

deleted theorem Bimon.ofMonComonObjX_one

deleted theorem Bimon.ofMonComon_toMonComon_obj_comul

deleted theorem Bimon.ofMonComon_toMonComon_obj_counit

deleted theorem Bimon.one_comul

deleted def Bimon.toComon

deleted theorem Bimon.toComon_forget

deleted def Bimon.toMonComon

deleted def Bimon.toMonComonObj

deleted theorem Bimon.toMonComon_ofMonComon_obj_mul

deleted theorem Bimon.toMonComon_ofMonComon_obj_one

deleted theorem Bimon.toMon_forget

deleted def Bimon.toTrivial

deleted def Bimon.trivial

deleted def Bimon.trivialTo

deleted def Bimon

added theorem CategoryTheory.Bimon.BimonObjAux_comul

added theorem CategoryTheory.Bimon.BimonObjAux_counit

added theorem CategoryTheory.Bimon.comp_hom'

added theorem CategoryTheory.Bimon.compatibility

added def CategoryTheory.Bimon.equivMonComon

added def CategoryTheory.Bimon.equivMonComonCounitIsoApp

added def CategoryTheory.Bimon.equivMonComonCounitIsoAppX

added def CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux

added def CategoryTheory.Bimon.equivMonComonUnitIsoApp

added def CategoryTheory.Bimon.equivMonComonUnitIsoAppX

added def CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux

added theorem CategoryTheory.Bimon.ext

added def CategoryTheory.Bimon.forget

added theorem CategoryTheory.Bimon.id_hom'

added def CategoryTheory.Bimon.mk'

added def CategoryTheory.Bimon.mk'X

added theorem CategoryTheory.Bimon.mul_counit

added def CategoryTheory.Bimon.ofMonComon

added def CategoryTheory.Bimon.ofMonComonObj

added def CategoryTheory.Bimon.ofMonComonObjX

added theorem CategoryTheory.Bimon.ofMonComonObjX_mul

added theorem CategoryTheory.Bimon.ofMonComonObjX_one

added theorem CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul

added theorem CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit

added theorem CategoryTheory.Bimon.one_comul

added def CategoryTheory.Bimon.toComon

added theorem CategoryTheory.Bimon.toComon_forget

added def CategoryTheory.Bimon.toMonComon

added def CategoryTheory.Bimon.toMonComonObj

added theorem CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul

added theorem CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one

added theorem CategoryTheory.Bimon.toMon_forget

added def CategoryTheory.Bimon.toTrivial

added def CategoryTheory.Bimon.trivial

added def CategoryTheory.Bimon.trivialTo

added def CategoryTheory.Bimon

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

added def CategoryTheory.CommGrpObj.ofRepresentableBy

deleted def CommGrpObj.ofRepresentableBy

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

added theorem CategoryTheory.IsCommMonObj.ofRepresentableBy

deleted theorem IsCommMonObj.ofRepresentableBy

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

added def CategoryTheory.cartesianComon

added def CategoryTheory.comonEquiv

added theorem CategoryTheory.comul_eq_lift

added theorem CategoryTheory.counit_eq_toUnit

added def CategoryTheory.isoCartesianComon

deleted def cartesianComon

deleted def comonEquiv

deleted theorem comul_eq_lift

deleted theorem counit_eq_toUnit

deleted def isoCartesianComon

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

added def CategoryTheory.Grp.homMk

added theorem CategoryTheory.Grp.homMk_hom'

added theorem CategoryTheory.GrpObj.comp_div

added theorem CategoryTheory.GrpObj.comp_inv

added theorem CategoryTheory.GrpObj.comp_zpow

added theorem CategoryTheory.GrpObj.div_comp

added theorem CategoryTheory.GrpObj.inv_comp

added theorem CategoryTheory.GrpObj.inv_eq_inv

added def CategoryTheory.GrpObj.ofRepresentableBy

added theorem CategoryTheory.GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy

added theorem CategoryTheory.GrpObj.one_inv

added theorem CategoryTheory.GrpObj.zpow_comp

added theorem CategoryTheory.Hom.inv_def

added theorem CategoryTheory.essImage_yonedaGrp

added def CategoryTheory.yonedaGrp

added def CategoryTheory.yonedaGrpFullyFaithful

added def CategoryTheory.yonedaGrpObj

added def CategoryTheory.yonedaGrpObjIsoOfRepresentableBy

added def CategoryTheory.yonedaGrpObjRepresentableBy

added theorem CategoryTheory.yonedaGrp_naturality

deleted def Grp.homMk

deleted theorem Grp.homMk_hom'

deleted theorem GrpObj.comp_div

deleted theorem GrpObj.comp_inv

deleted theorem GrpObj.comp_zpow

deleted theorem GrpObj.div_comp

deleted theorem GrpObj.inv_comp

deleted theorem GrpObj.inv_eq_inv

deleted def GrpObj.ofRepresentableBy

deleted theorem GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy

deleted theorem GrpObj.one_inv

deleted theorem GrpObj.zpow_comp

deleted theorem Hom.inv_def

deleted theorem essImage_yonedaGrp

deleted def yonedaGrp

deleted def yonedaGrpFullyFaithful

deleted def yonedaGrpObj

deleted def yonedaGrpObjIsoOfRepresentableBy

deleted def yonedaGrpObjRepresentableBy

deleted theorem yonedaGrp_naturality

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

added def CategoryTheory.ModObj.trivialAction

added def CategoryTheory.Mod_.trivialAction

deleted def ModObj.trivialAction

deleted def Mod_.trivialAction

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

added def CategoryTheory.Hom.mulEquivCongrRight

added theorem CategoryTheory.Hom.mul_def

added theorem CategoryTheory.Hom.one_def

added theorem CategoryTheory.Mon.fst_hom

added theorem CategoryTheory.Mon.lift_hom

added theorem CategoryTheory.Mon.snd_hom

added theorem CategoryTheory.MonObj.comp_mul

added theorem CategoryTheory.MonObj.comp_one

added theorem CategoryTheory.MonObj.comp_pow

added theorem CategoryTheory.MonObj.lift_comp_one_left

added theorem CategoryTheory.MonObj.lift_comp_one_right

added theorem CategoryTheory.MonObj.lift_lift_assoc

added theorem CategoryTheory.MonObj.mul_comp

added theorem CategoryTheory.MonObj.mul_eq_mul

added def CategoryTheory.MonObj.ofRepresentableBy

added theorem CategoryTheory.MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy

added theorem CategoryTheory.MonObj.one_comp

added theorem CategoryTheory.MonObj.one_eq_one

added theorem CategoryTheory.MonObj.pow_comp

added theorem CategoryTheory.essImage_yonedaMon

added def CategoryTheory.yonedaMon

added def CategoryTheory.yonedaMonFullyFaithful

added def CategoryTheory.yonedaMonObj

added def CategoryTheory.yonedaMonObjIsoOfRepresentableBy

added def CategoryTheory.yonedaMonObjRepresentableBy

added theorem CategoryTheory.yonedaMon_naturality

deleted def Hom.mulEquivCongrRight

deleted theorem Hom.mul_def

deleted theorem Hom.one_def

deleted theorem Mon.fst_hom

deleted theorem Mon.lift_hom

deleted theorem Mon.snd_hom

deleted theorem MonObj.comp_mul

deleted theorem MonObj.comp_one

deleted theorem MonObj.comp_pow

deleted theorem MonObj.lift_comp_one_left

deleted theorem MonObj.lift_comp_one_right

deleted theorem MonObj.lift_lift_assoc

deleted theorem MonObj.mul_comp

deleted theorem MonObj.mul_eq_mul

deleted def MonObj.ofRepresentableBy

deleted theorem MonObj.ofRepresentableBy_yonedaMonObjRepresentableBy

deleted theorem MonObj.one_comp

deleted theorem MonObj.one_eq_one

deleted theorem MonObj.pow_comp

deleted theorem essImage_yonedaMon

deleted def yonedaMon

deleted def yonedaMonFullyFaithful

deleted def yonedaMonObj

deleted def yonedaMonObjIsoOfRepresentableBy

deleted def yonedaMonObjRepresentableBy

deleted theorem yonedaMon_naturality

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

added theorem CategoryTheory.CommGrp.comp'

added theorem CategoryTheory.CommGrp.comp_hom

added def CategoryTheory.CommGrp.forget

added def CategoryTheory.CommGrp.forget₂CommMon

added theorem CategoryTheory.CommGrp.forget₂CommMon_comp_forget

added theorem CategoryTheory.CommGrp.forget₂CommMon_map_hom

added theorem CategoryTheory.CommGrp.forget₂CommMon_obj_mul

added theorem CategoryTheory.CommGrp.forget₂CommMon_obj_one

added def CategoryTheory.CommGrp.forget₂Grp

added theorem CategoryTheory.CommGrp.forget₂Grp_comp_forget

added theorem CategoryTheory.CommGrp.forget₂Grp_map_hom

added theorem CategoryTheory.CommGrp.forget₂Grp_obj_mul

added theorem CategoryTheory.CommGrp.forget₂Grp_obj_one

added def CategoryTheory.CommGrp.fullyFaithfulForget₂CommMon

added def CategoryTheory.CommGrp.fullyFaithfulForget₂Grp

added theorem CategoryTheory.CommGrp.hom_ext

added theorem CategoryTheory.CommGrp.id'

added theorem CategoryTheory.CommGrp.id_hom

added def CategoryTheory.CommGrp.mkIso'

added def CategoryTheory.CommGrp.toCommMon

added def CategoryTheory.CommGrp.toGrp

added def CategoryTheory.CommGrp.trivial

added structure CategoryTheory.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/CommMon_.lean

added def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided

added def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj

added theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε

added theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ

added def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso

added theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul

added theorem CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one

added def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon

added def CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso

added theorem CategoryTheory.CommMon.comp'

added theorem CategoryTheory.CommMon.comp_hom

added def CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit

added def CategoryTheory.CommMon.forget

added def CategoryTheory.CommMon.forget₂Mon

added theorem CategoryTheory.CommMon.forget₂Mon_comp_forget

added theorem CategoryTheory.CommMon.forget₂Mon_map_hom

added theorem CategoryTheory.CommMon.forget₂Mon_obj_mul

added theorem CategoryTheory.CommMon.forget₂Mon_obj_one

added def CategoryTheory.CommMon.fullyFaithfulForget₂Mon

added theorem CategoryTheory.CommMon.hom_ext

added theorem CategoryTheory.CommMon.id'

added theorem CategoryTheory.CommMon.id_hom

added def CategoryTheory.CommMon.mkIso'

added def CategoryTheory.CommMon.toMon

added def CategoryTheory.CommMon.trivial

added structure CategoryTheory.CommMon

deleted def CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided

deleted def CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj

deleted theorem CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε

deleted theorem CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ

deleted def CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.counitIso

deleted theorem CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul

deleted theorem CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one

deleted def CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon

deleted def CategoryTheory.Equivalence.CommMon.EquivLaxBraidedFunctorPUnit.unitIso

deleted def CategoryTheory.Equivalence.CommMon.equivLaxBraidedFunctorPUnit

deleted theorem CommMon.comp'

deleted theorem CommMon.comp_hom

deleted def CommMon.forget

deleted def CommMon.forget₂Mon

deleted theorem CommMon.forget₂Mon_comp_forget

deleted theorem CommMon.forget₂Mon_map_hom

deleted theorem CommMon.forget₂Mon_obj_mul

deleted theorem CommMon.forget₂Mon_obj_one

deleted def CommMon.fullyFaithfulForget₂Mon

deleted theorem CommMon.hom_ext

deleted theorem CommMon.id'

deleted theorem CommMon.id_hom

deleted def CommMon.mkIso'

deleted def CommMon.toMon

deleted def CommMon.trivial

deleted structure CommMon

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

added def CategoryTheory.Comon.ComonToMonOpOp

added def CategoryTheory.Comon.ComonToMonOpOpObj

added def CategoryTheory.Comon.Comon_EquivMon_OpOp

added structure CategoryTheory.Comon.Hom

added def CategoryTheory.Comon.MonOpOpToComon

added def CategoryTheory.Comon.MonOpOpToComonObj

added def CategoryTheory.Comon.comp

added theorem CategoryTheory.Comon.comp_hom'

added theorem CategoryTheory.Comon.ext

added def CategoryTheory.Comon.forget

added theorem CategoryTheory.Comon.forget_δ

added theorem CategoryTheory.Comon.forget_ε

added theorem CategoryTheory.Comon.forget_η

added theorem CategoryTheory.Comon.forget_μ

added def CategoryTheory.Comon.id

added theorem CategoryTheory.Comon.id_hom'

added def CategoryTheory.Comon.mkIso'

added def CategoryTheory.Comon.mkIso

added theorem CategoryTheory.Comon.tensorObj_X

added theorem CategoryTheory.Comon.tensorObj_comul'

added theorem CategoryTheory.Comon.tensorObj_comul

added theorem CategoryTheory.Comon.tensorObj_counit

added def CategoryTheory.Comon.trivial

added structure CategoryTheory.Comon

added theorem CategoryTheory.ComonObj.comul_assoc_flip

added theorem CategoryTheory.ComonObj.comul_counit_hom

added theorem CategoryTheory.ComonObj.counit_comul_hom

added def CategoryTheory.ComonObj.instTensorUnit

deleted def Comon.ComonToMonOpOp

deleted def Comon.ComonToMonOpOpObj

deleted def Comon.Comon_EquivMon_OpOp

deleted structure Comon.Hom

deleted def Comon.MonOpOpToComon

deleted def Comon.MonOpOpToComonObj

deleted def Comon.comp

deleted theorem Comon.comp_hom'

deleted theorem Comon.ext

deleted def Comon.forget

deleted theorem Comon.forget_δ

deleted theorem Comon.forget_ε

deleted theorem Comon.forget_η

deleted theorem Comon.forget_μ

deleted def Comon.id

deleted theorem Comon.id_hom'

deleted def Comon.mkIso'

deleted def Comon.mkIso

deleted theorem Comon.tensorObj_X

deleted theorem Comon.tensorObj_comul'

deleted theorem Comon.tensorObj_comul

deleted theorem Comon.tensorObj_counit

deleted def Comon.trivial

deleted structure Comon

deleted theorem ComonObj.comul_assoc_flip

deleted theorem ComonObj.comul_counit_hom

deleted theorem ComonObj.counit_comul_hom

deleted def ComonObj.instTensorUnit

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

added theorem CategoryTheory.Grp.comp'

added theorem CategoryTheory.Grp.comp_hom

added theorem CategoryTheory.Grp.hom_ext

added theorem CategoryTheory.Grp.id'

added theorem CategoryTheory.Grp.id_hom

added def CategoryTheory.Grp.toMon

added def CategoryTheory.Grp.trivial

added structure CategoryTheory.Grp

added theorem CategoryTheory.GrpObj.eq_lift_inv_left

added theorem CategoryTheory.GrpObj.eq_lift_inv_right

added theorem CategoryTheory.GrpObj.ext

added theorem CategoryTheory.GrpObj.inv_comp_inv

added theorem CategoryTheory.GrpObj.inv_hom

added theorem CategoryTheory.GrpObj.inv_inv

added theorem CategoryTheory.GrpObj.isPullback

added theorem CategoryTheory.GrpObj.lift_comp_inv_left

added theorem CategoryTheory.GrpObj.lift_comp_inv_right

added theorem CategoryTheory.GrpObj.lift_inv_comp_left

added theorem CategoryTheory.GrpObj.lift_inv_comp_right

added theorem CategoryTheory.GrpObj.lift_inv_left_eq

added theorem CategoryTheory.GrpObj.lift_inv_right_eq

added theorem CategoryTheory.GrpObj.lift_left_mul_ext

added def CategoryTheory.GrpObj.mulRight

added theorem CategoryTheory.GrpObj.mulRight_one

added theorem CategoryTheory.GrpObj.mul_inv

added theorem CategoryTheory.GrpObj.mul_inv_rev

added theorem CategoryTheory.GrpObj.tensorHom_inv_inv_mul

added def CategoryTheory.GrpObj.tensorObj.Adjunction.mapGrp

added def CategoryTheory.GrpObj.tensorObj.Equivalence.mapGrp

added theorem CategoryTheory.GrpObj.tensorObj.Functor.comp_mapGrp_mul

added theorem CategoryTheory.GrpObj.tensorObj.Functor.comp_mapGrp_one

added theorem CategoryTheory.GrpObj.tensorObj.Functor.essImage_mapGrp

added def CategoryTheory.GrpObj.tensorObj.Functor.mapGrp

added def CategoryTheory.GrpObj.tensorObj.Functor.mapGrpCompIso

added def CategoryTheory.GrpObj.tensorObj.Functor.mapGrpIdIso

added def CategoryTheory.GrpObj.tensorObj.Functor.mapGrpNatIso

added def CategoryTheory.GrpObj.tensorObj.Functor.mapGrpNatTrans

added theorem CategoryTheory.GrpObj.tensorObj.Functor.mapGrp_id_mul

added theorem CategoryTheory.GrpObj.tensorObj.Functor.mapGrp_id_one

added theorem CategoryTheory.GrpObj.tensorObj.Functor.obj.ι_def

added theorem CategoryTheory.GrpObj.tensorObj.Grp.associator_hom_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.associator_inv_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.braiding_hom_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.braiding_inv_hom

added def CategoryTheory.GrpObj.tensorObj.Grp.forget

added def CategoryTheory.GrpObj.tensorObj.Grp.forget₂Mon

added theorem CategoryTheory.GrpObj.tensorObj.Grp.forget₂Mon_comp_forget

added theorem CategoryTheory.GrpObj.tensorObj.Grp.forget₂Mon_map_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.forget₂Mon_obj_mul

added theorem CategoryTheory.GrpObj.tensorObj.Grp.forget₂Mon_obj_one

added theorem CategoryTheory.GrpObj.tensorObj.Grp.fst_hom

added def CategoryTheory.GrpObj.tensorObj.Grp.fullyFaithfulForget₂Mon

added theorem CategoryTheory.GrpObj.tensorObj.Grp.leftUnitor_hom_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.leftUnitor_inv_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.lift_hom

added def CategoryTheory.GrpObj.tensorObj.Grp.mkIso'

added theorem CategoryTheory.GrpObj.tensorObj.Grp.rightUnitor_hom_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.rightUnitor_inv_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.snd_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorObj_mul

added theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorObj_one

added theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorUnit_X

added theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorUnit_mul

added theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorUnit_one

added theorem CategoryTheory.GrpObj.tensorObj.Grp.whiskerLeft_hom

added theorem CategoryTheory.GrpObj.tensorObj.Grp.whiskerRight_hom

added theorem CategoryTheory.GrpObj.toMonObj_injective

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

deleted theorem GrpObj.eq_lift_inv_left

deleted theorem GrpObj.eq_lift_inv_right

deleted theorem GrpObj.ext

deleted theorem GrpObj.inv_comp_inv

deleted theorem GrpObj.inv_hom

deleted theorem GrpObj.inv_inv

deleted theorem GrpObj.isPullback

deleted theorem GrpObj.lift_comp_inv_left

deleted theorem GrpObj.lift_comp_inv_right

deleted theorem GrpObj.lift_inv_comp_left

deleted theorem GrpObj.lift_inv_comp_right

deleted theorem GrpObj.lift_inv_left_eq

deleted theorem GrpObj.lift_inv_right_eq

deleted theorem GrpObj.lift_left_mul_ext

deleted def GrpObj.mulRight

deleted theorem GrpObj.mulRight_one

deleted theorem GrpObj.mul_inv

deleted theorem GrpObj.mul_inv_rev

deleted theorem GrpObj.tensorHom_inv_inv_mul

deleted def GrpObj.tensorObj.CategoryTheory.Adjunction.mapGrp

deleted def GrpObj.tensorObj.CategoryTheory.Equivalence.mapGrp

deleted theorem GrpObj.tensorObj.CategoryTheory.Functor.comp_mapGrp_mul

deleted theorem GrpObj.tensorObj.CategoryTheory.Functor.comp_mapGrp_one

deleted theorem GrpObj.tensorObj.CategoryTheory.Functor.essImage_mapGrp

deleted def GrpObj.tensorObj.CategoryTheory.Functor.mapGrp

deleted def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpCompIso

deleted def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpIdIso

deleted def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpNatIso

deleted def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpNatTrans

deleted theorem GrpObj.tensorObj.CategoryTheory.Functor.mapGrp_id_mul

deleted theorem GrpObj.tensorObj.CategoryTheory.Functor.mapGrp_id_one

deleted theorem GrpObj.tensorObj.CategoryTheory.Functor.obj.ι_def

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 GrpObj.toMonObj_injective

Modified Mathlib/CategoryTheory/Monoidal/Hopf_.lean

added def CategoryTheory.Hopf.toBimon

added structure CategoryTheory.Hopf

added theorem CategoryTheory.HopfObj.antipode_antipode

added theorem CategoryTheory.HopfObj.antipode_comul

added theorem CategoryTheory.HopfObj.antipode_comul₁

added theorem CategoryTheory.HopfObj.antipode_comul₂

added theorem CategoryTheory.HopfObj.antipode_counit

added theorem CategoryTheory.HopfObj.hom_antipode

added theorem CategoryTheory.HopfObj.mul_antipode

added theorem CategoryTheory.HopfObj.mul_antipode₁

added theorem CategoryTheory.HopfObj.mul_antipode₂

added theorem CategoryTheory.HopfObj.one_antipode

deleted def Hopf.toBimon

deleted structure Hopf

deleted theorem HopfObj.antipode_antipode

deleted theorem HopfObj.antipode_comul

deleted theorem HopfObj.antipode_comul₁

deleted theorem HopfObj.antipode_comul₂

deleted theorem HopfObj.antipode_counit

deleted theorem HopfObj.hom_antipode

deleted theorem HopfObj.mul_antipode

deleted theorem HopfObj.mul_antipode₁

deleted theorem HopfObj.mul_antipode₂

deleted theorem HopfObj.one_antipode

Modified Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

added def CategoryTheory.Mon.forgetMapConeLimitConeIso

added def CategoryTheory.Mon.limit

added def CategoryTheory.Mon.limitCone

added def CategoryTheory.Mon.limitConeIsLimit

deleted def Mon.forgetMapConeLimitConeIso

deleted def Mon.limit

deleted def Mon.limitCone

deleted def Mon.limitConeIsLimit

Modified Mathlib/CategoryTheory/Monoidal/Mod_.lean

added theorem CategoryTheory.ModObj.assoc_flip

added theorem CategoryTheory.ModObj.ext

added theorem CategoryTheory.ModObj.mul_smul

added theorem CategoryTheory.ModObj.one_smul

added theorem CategoryTheory.ModObj.smul_eq_mul

added def CategoryTheory.Mod_.Hom.mk''

added def CategoryTheory.Mod_.Hom.mk'

added structure CategoryTheory.Mod_.Hom

added theorem CategoryTheory.Mod_.assoc_flip

added def CategoryTheory.Mod_.comap

added def CategoryTheory.Mod_.comp

added theorem CategoryTheory.Mod_.comp_hom'

added def CategoryTheory.Mod_.forget

added theorem CategoryTheory.Mod_.hom_ext

added def CategoryTheory.Mod_.id

added theorem CategoryTheory.Mod_.id_hom'

added def CategoryTheory.Mod_.regular

added def CategoryTheory.Mod_.scalarRestriction

added theorem CategoryTheory.Mod_.scalarRestriction_hom

added structure CategoryTheory.Mod_

deleted theorem ModObj.assoc_flip

deleted theorem ModObj.ext

deleted theorem ModObj.mul_smul

deleted theorem ModObj.one_smul

deleted theorem ModObj.smul_eq_mul

deleted def Mod_.Hom.mk''

deleted def Mod_.Hom.mk'

deleted structure Mod_.Hom

deleted theorem Mod_.assoc_flip

deleted def Mod_.comap

deleted def Mod_.comp

deleted theorem Mod_.comp_hom'

deleted def Mod_.forget

deleted theorem Mod_.hom_ext

deleted def Mod_.id

deleted theorem Mod_.id_hom'

deleted def Mod_.regular

deleted def Mod_.scalarRestriction

deleted theorem Mod_.scalarRestriction_hom

deleted structure Mod_

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

deleted theorem CategoryTheory.Equivalence.IsCommMonObj.mul_comm'

deleted def CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.counitIso

deleted def CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux

deleted theorem CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux

deleted def CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon

deleted def CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal

deleted def CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj

deleted theorem CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε

deleted theorem CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ

deleted theorem CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul

deleted theorem CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one

deleted def CategoryTheory.Equivalence.Mon.EquivLaxMonoidalFunctorPUnit.unitIso

deleted def CategoryTheory.Equivalence.Mon.equivLaxMonoidalFunctorPUnit

deleted theorem CategoryTheory.Equivalence.MonObj.mul_mul_mul_comm'

deleted theorem CategoryTheory.Equivalence.MonObj.mul_mul_mul_comm

added theorem CategoryTheory.IsCommMonObj.mul_comm'

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv

added theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul

added def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso

added def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux

added theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux

added def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon

added def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal

added def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj

added theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε

added theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ

added theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul

added theorem CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one

added def CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso

added theorem CategoryTheory.Mon.Hom.ext'

added structure CategoryTheory.Mon.Hom

added theorem CategoryTheory.Mon.associator_hom_hom

added theorem CategoryTheory.Mon.associator_inv_hom

added theorem CategoryTheory.Mon.braiding_hom_hom

added theorem CategoryTheory.Mon.braiding_inv_hom

added def CategoryTheory.Mon.comp

added theorem CategoryTheory.Mon.comp_hom'

added def CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit

added def CategoryTheory.Mon.forget

added theorem CategoryTheory.Mon.forget_δ

added theorem CategoryTheory.Mon.forget_ε

added theorem CategoryTheory.Mon.forget_η

added theorem CategoryTheory.Mon.forget_μ

added theorem CategoryTheory.Mon.hom_injective

added def CategoryTheory.Mon.id

added theorem CategoryTheory.Mon.id_hom'

added theorem CategoryTheory.Mon.leftUnitor_hom_hom

added theorem CategoryTheory.Mon.leftUnitor_inv_hom

added def CategoryTheory.Mon.mkIso'

added theorem CategoryTheory.Mon.rightUnitor_hom_hom

added theorem CategoryTheory.Mon.rightUnitor_inv_hom

added theorem CategoryTheory.Mon.tensorObj_mul

added theorem CategoryTheory.Mon.tensorObj_one

added theorem CategoryTheory.Mon.tensorUnit_X

added theorem CategoryTheory.Mon.tensorUnit_mul

added theorem CategoryTheory.Mon.tensorUnit_one

added theorem CategoryTheory.Mon.tensor_mul

added theorem CategoryTheory.Mon.tensor_one

added def CategoryTheory.Mon.trivial

added theorem CategoryTheory.Mon.whiskerLeft_hom

added theorem CategoryTheory.Mon.whiskerRight_hom

added structure CategoryTheory.Mon

added theorem CategoryTheory.MonObj.Mon_tensor_mul_assoc

added theorem CategoryTheory.MonObj.Mon_tensor_mul_one

added theorem CategoryTheory.MonObj.Mon_tensor_one_mul

added theorem CategoryTheory.MonObj.ext

added theorem CategoryTheory.MonObj.mul_assoc_flip

added theorem CategoryTheory.MonObj.mul_associator

added theorem CategoryTheory.MonObj.mul_braiding

added theorem CategoryTheory.MonObj.mul_leftUnitor

added theorem CategoryTheory.MonObj.mul_mul_mul_comm'

added theorem CategoryTheory.MonObj.mul_mul_mul_comm

added theorem CategoryTheory.MonObj.mul_one_hom

added theorem CategoryTheory.MonObj.mul_rightUnitor

added def CategoryTheory.MonObj.ofIso

added theorem CategoryTheory.MonObj.one_associator

added theorem CategoryTheory.MonObj.one_braiding

added theorem CategoryTheory.MonObj.one_leftUnitor

added theorem CategoryTheory.MonObj.one_mul_hom

added theorem CategoryTheory.MonObj.one_rightUnitor

deleted theorem Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom

deleted theorem Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp

deleted theorem Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom

deleted theorem Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp

deleted theorem Mathlib.Tactic.MonTauto.eq_mul_one

deleted theorem Mathlib.Tactic.MonTauto.eq_one_mul

deleted theorem Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul

deleted theorem Mathlib.Tactic.MonTauto.mul_assoc_hom

deleted theorem Mathlib.Tactic.MonTauto.mul_assoc_inv

deleted theorem Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul

deleted theorem Mon.Hom.ext'

deleted structure Mon.Hom

deleted theorem Mon.associator_hom_hom

deleted theorem Mon.associator_inv_hom

deleted theorem Mon.braiding_hom_hom

deleted theorem Mon.braiding_inv_hom

deleted def Mon.comp

deleted theorem Mon.comp_hom'

deleted def Mon.forget

deleted theorem Mon.forget_δ

deleted theorem Mon.forget_ε

deleted theorem Mon.forget_η

deleted theorem Mon.forget_μ

deleted theorem Mon.hom_injective

deleted def Mon.id

deleted theorem Mon.id_hom'

deleted theorem Mon.leftUnitor_hom_hom

deleted theorem Mon.leftUnitor_inv_hom

deleted def Mon.mkIso'

deleted theorem Mon.rightUnitor_hom_hom

deleted theorem Mon.rightUnitor_inv_hom

deleted theorem Mon.tensorObj_mul

deleted theorem Mon.tensorObj_one

deleted theorem Mon.tensorUnit_X

deleted theorem Mon.tensorUnit_mul

deleted theorem Mon.tensorUnit_one

deleted theorem Mon.tensor_mul

deleted theorem Mon.tensor_one

deleted def Mon.trivial

deleted theorem Mon.whiskerLeft_hom

deleted theorem Mon.whiskerRight_hom

deleted structure Mon

deleted theorem MonObj.Mon_tensor_mul_assoc

deleted theorem MonObj.Mon_tensor_mul_one

deleted theorem MonObj.Mon_tensor_one_mul

deleted theorem MonObj.ext

deleted theorem MonObj.mul_assoc_flip

deleted theorem MonObj.mul_associator

deleted theorem MonObj.mul_braiding

deleted theorem MonObj.mul_leftUnitor

deleted theorem MonObj.mul_one_hom

deleted theorem MonObj.mul_rightUnitor

deleted def MonObj.ofIso

deleted theorem MonObj.one_associator

deleted theorem MonObj.one_braiding

deleted theorem MonObj.one_leftUnitor

deleted theorem MonObj.one_mul_hom

deleted theorem MonObj.one_rightUnitor