Theorems · Definition · Lie groups
ProfiniteGrp.toProfinite
ProfiniteGrp.{u} → ProfiniteThe underlying profinite topological space.
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Profinitestatement · cited by 75
- ProfiniteGrpstatement and proof · cited by 47
Cited by85
Results whose statement or proof uses this declaration.
- ProfiniteGrp.limitproof · cited by 23
- ProfiniteGrp.Hom.homstatement · cited by 20
- ProfiniteGrp.limitConePtAuxstatement and proof · cited by 19
- ProfiniteGrp.diagramstatement · cited by 10
- ProfiniteGrp.ProfiniteCompletion.etastatement · cited by 6
- InfiniteGalois.projstatement and proof · cited by 6
- ProfiniteGrp.isoLimittoFiniteQuotientFunctorstatement · cited by 3
- ProfiniteGrp.toFiniteQuotientFunctorstatement and proof · cited by 3
- ProfiniteGrp.toLimitstatement and proof · cited by 3
- InfiniteGalois.limitToAlgEquivstatement and proof · cited by 3
- ProfiniteGrp.ProfiniteCompletion.liftstatement and proof · cited by 3
- InfiniteGalois.mulEquivToLimitstatement and proof · cited by 3