Commit 2024-09-17 15:51 2f37c5dc

View on Github →

feat(Topology/Group/Profinite): Define Profinite Groups (#16648) Define Profinite Groups

Estimated changes

added structure FiniteAddGrp
added def FiniteGrp.of
added def FiniteGrp.ofHom
added theorem FiniteGrp.ofHom_apply
added structure FiniteGrp
added structure ProfiniteAddGrp
added theorem ProfiniteGrp.coe_comp
added theorem ProfiniteGrp.coe_id
added theorem ProfiniteGrp.coe_of
added def ProfiniteGrp.of
added def ProfiniteGrp.pi
added structure ProfiniteGrp
added def Profinite.pi