instZPow — Mathlib

English

If G is a Group with IsTopologicalGroup, then SeparationQuotient G has a Pow structure for integers.

Русский

Если G — группа с IsTopologicalGroup, SeparationQuotient(G) обладает степенным оператором для целых.

LaTeX

$$$\operatorname{Pow}(\mathrm{SeparationQuotient}(G))\, \mathbb{Z}$$$

Lean4

@[to_additive existing]
instance instZPow [Group G] [IsTopologicalGroup G] : Pow (SeparationQuotient G) ℤ where
  pow x n := Quotient.map' (s₁ := inseparableSetoid G) (· ^ n) (fun _ _ h ↦ Inseparable.zpow h n) x

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