Documentation Verification Report

ProfiniteGrp

📁 Source: MathlibTest/CategoryTheory/ConcreteCategory/ProfiniteGrp.lean

Statistics

Metric	Count
Definitions `ProfiniteGrp`	1
Theorems	0
Total	1

(root)

Definitions

Name	Category	Theorems
`ProfiniteGrp` 📖	CompData	41 math math: `ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.ofHom_comp`, `ProfiniteGrp.limit_one_val`, `ProfiniteGrp.ProfiniteCompletion.lift_eta`, `ProfiniteGrp.coe_id`, `ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc`, `InfiniteGalois.toAlgEquivAux_eq_proj_of_mem`, `ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.hom_id`, `ProfiniteGrp.denseRange_toLimit`, `ProfiniteGrp.instHasLimit`, `ProfiniteGrp.comp_apply`, `ProfiniteGrp.hom_comp`, `InfiniteGalois.mulEquivToLimit_symm_continuous`, `ProfiniteGrp.inv_hom_apply`, `InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup`, `ProfiniteGrp.cone_pt`, `InfiniteGalois.proj_adjoin_singleton_val`, `ProfiniteGrp.limit_mul_val`, `ProfiniteGrp.profiniteCompletion_map`, `ProfiniteGrp.hom_inv_apply`, `ProfiniteGrp.cone_π_app`, `InfiniteGalois.toAlgEquivAux_eq_liftNormal`, `ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `ProfiniteGrp.ofHom_id`, `ProfiniteGrp.coe_comp`, `InfiniteGalois.mk_toAlgEquivAux`, `InfiniteGalois.proj_of_le`, `ProfiniteGrp.toLimitFun_continuous`, `ProfiniteGrp.diagram_map`, `InfiniteGalois.algEquivToLimit_continuous`, `ProfiniteGrp.id_apply`, `ProfiniteGrp.isIso_toLimit`, `InfiniteGalois.limitToAlgEquiv_symm_apply`, `ProfiniteGrp.profiniteCompletion_obj`, `ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap`, `ProfiniteGrp.limit_ext_iff`, `ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap`, `ProfiniteGrp.diagram_obj`, `ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite`

---

← Back to Index