Theorems · Definition · Lie groups

ProfiniteAddGrp.ofContinuousAddEquiv

{G : ProfiniteAddGrp.{u}} →
  {H : Type v} →
    [inst : TopologicalSpace H] →
      [inst_1 : AddGroup H] → [IsTopologicalAddGroup H] → ↑G.toProfinite.toTop ≃ₜ+ H → ProfiniteAddGrp.{v}

A topological additive group that has a ContinuousAddEquiv to a profinite additive group is profinite.

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupIsTopologicalAddGroup