Theorems · Definition · Lie groups

ProfiniteAddGrp.of

(G : Type u) →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalAddGroup G] → [CompactSpace G] → [TotallyDisconnectedSpace G] → ProfiniteAddGrp.{u}

Construct a term of ProfiniteAddGrp from a type endowed with the structure of a compact and totally disconnected topological additive group. (The condition of being Hausdorff can be omitted here because totally disconnected implies that {0} is a closed set, thus implying Hausdorff in a topological additive group.)

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Cited by

6 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupCompactSpaceTotallyDisconnectedSpace