toProfiniteGrpIso — Mathlib

English

From a ContinuousMulEquiv between profinite groups X ≃ₜ* Y one obtains an isomorphism X ≅ Y in the category ProfiniteGrp.

Русский

Из непрерывного умножительного эквивалента между профинированными группами X и Y следует изоморфизм X ≅ Y в категории ProfiniteGrp.

LaTeX

$$$\forall X,Y\in \mathrm{ProfiniteGrp},\; e:X\simeq_{t*}Y \Rightarrow X\cong Y$ in ProfiniteGrp$$

Lean4

/-- Build an isomorphism in the category `ProfiniteGrp` from
a `ContinuousMulEquiv` between `ProfiniteGrp`s. -/
def toProfiniteGrpIso {X Y : ProfiniteGrp} (e : X ≃ₜ* Y) : X ≅ Y
    where
  hom := ofHom e
  inv := ofHom e.symm

Похожие утверждения