Commit 2024-06-20 02:11 2e6f6dff

View on Github →

chore: Rename to Grp (#3731) This is a proposal to rename what was in mathlib Group and in mathlib4 GroupCat to its literature name Grp. This has the advantage not to conflict with group that has been capitalised to Group and to be shorter.

Estimated changes

deleted theorem AddCommGroupCat.exact_iff
added theorem AddCommGrp.exact_iff
deleted def AddCommGroupCat.adj
added def AddCommGrp.adj
added def AddCommGrp.free
modified def CommMonCat.units
deleted def GroupCat.abelianize
deleted def GroupCat.adj
deleted def GroupCat.free
added def Grp.abelianize
added def Grp.adj
added def Grp.free
modified def MonCat.units
added def AddCommGrp.asHom
added theorem AddCommGrp.asHom_apply
added theorem AddCommGrp.int_hom_ext
deleted theorem CommGroupCat.coe_comp'
deleted theorem CommGroupCat.coe_comp
deleted theorem CommGroupCat.coe_id'
deleted theorem CommGroupCat.coe_id
deleted theorem CommGroupCat.coe_of
deleted theorem CommGroupCat.comp_def
deleted theorem CommGroupCat.ext
deleted theorem CommGroupCat.forget_map
deleted def CommGroupCat.of
deleted def CommGroupCat.ofHom
deleted theorem CommGroupCat.ofHom_apply
deleted theorem CommGroupCat.one_apply
deleted def CommGroupCat
added theorem CommGrp.coe_comp'
added theorem CommGrp.coe_comp
added theorem CommGrp.coe_id'
added theorem CommGrp.coe_id
added theorem CommGrp.coe_of
added theorem CommGrp.comp_def
added theorem CommGrp.ext
added theorem CommGrp.forget_map
added def CommGrp.of
added def CommGrp.ofHom
added theorem CommGrp.ofHom_apply
added theorem CommGrp.one_apply
added def CommGrp
deleted theorem GroupCat.coe_comp'
deleted theorem GroupCat.coe_comp
deleted theorem GroupCat.coe_id'
deleted theorem GroupCat.coe_id
deleted theorem GroupCat.coe_of
deleted theorem GroupCat.comp_def
deleted theorem GroupCat.ext
deleted theorem GroupCat.forget_map
deleted def GroupCat.of
deleted def GroupCat.ofHom
deleted theorem GroupCat.ofHom_apply
deleted theorem GroupCat.one_apply
deleted def GroupCat
added theorem Grp.coe_comp'
added theorem Grp.coe_comp
added theorem Grp.coe_id'
added theorem Grp.coe_id
added theorem Grp.coe_of
added theorem Grp.comp_def
added theorem Grp.ext
added theorem Grp.forget_map
added def Grp.of
added def Grp.ofHom
added theorem Grp.ofHom_apply
added theorem Grp.one_apply
added def Grp.uliftFunctor
added def Grp
added theorem MonoidHom.comp_id_grp
added theorem MonoidHom.id_grp_comp
modified def mulEquivIsoGroupIso
added theorem AddCommGrp.hasColimit
added theorem Grp.epi_iff_surjective
added theorem Grp.ker_eq_bot_of_mono
added theorem Grp.mono_iff_injective
added theorem Grp.surjective_of_epi
added def AddGrp.toGrp
added def Grp.toAddGrp
deleted theorem AddCommGroupCat.image.fac
added theorem AddCommGrp.image.fac
added def AddCommGrp.image
deleted theorem GroupWithZeroCat.coe_comp
deleted theorem GroupWithZeroCat.coe_id
deleted def GroupWithZeroCat.of
deleted def GroupWithZeroCat
added theorem GrpWithZero.coe_comp
added theorem GrpWithZero.coe_id
added theorem GrpWithZero.forget_map
added def GrpWithZero.of
added def GrpWithZero
modified def ModuleCat.mkOfSMul'
modified def ModuleCat.smul
modified def MonCat.adjoinOne
modified def MonCat.adjoinOneAdj
deleted theorem SemigroupCat.coe_of
deleted def SemigroupCat.of
deleted def SemigroupCat.ofHom
deleted theorem SemigroupCat.ofHom_apply
deleted def SemigroupCat
added theorem Semigrp.coe_of
added def Semigrp.of
added def Semigrp.ofHom
added theorem Semigrp.ofHom_apply
added def Semigrp
deleted theorem SemiNormedGroupCat.coe_id
deleted theorem SemiNormedGroupCat.coe_of
deleted theorem SemiNormedGroupCat.ext
deleted def SemiNormedGroupCat
added theorem SemiNormedGrp.coe_comp
added theorem SemiNormedGrp.coe_id
added theorem SemiNormedGrp.coe_of
added theorem SemiNormedGrp.ext
added def SemiNormedGrp.of
added def SemiNormedGrp
added def SemiNormedGrp₁
modified def Action.trivial
modified def Action.ρAut