Commit 2025-01-31 11:58 5c261c97

View on Github →

refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) Refactor morphisms in ProfiniteGrp into one-field structure.

Estimated changes

added structure ProfiniteAddGrp.Hom
added structure ProfiniteGrp.Hom
modified theorem ProfiniteGrp.coe_of
added theorem ProfiniteGrp.hom_comp
added theorem ProfiniteGrp.hom_ext
added theorem ProfiniteGrp.hom_id
added theorem ProfiniteGrp.hom_ofHom
added theorem ProfiniteGrp.id_apply
modified def ProfiniteGrp.of
added theorem ProfiniteGrp.ofHom_hom
added theorem ProfiniteGrp.ofHom_id