instZPow — Mathlib

English

There is a Pow (ℤ) instance on the unit sphere: for x in the unit sphere, x^n lies again in the unit sphere for any integer n.

Русский

На единичной сфере существует возведение в целочисленную степень: для x на единичной сфере x^n снова принадлежит единичной сфере при любом целочисленном n.

LaTeX

$$$\text{Pow} (S) \;\; (x,y) \text{ yields } x^n \in S \text{ for } n \in \mathbb{Z}$$$

Lean4

instance instZPow [NormedDivisionRing 𝕜] : Pow (sphere (0 : 𝕜) 1) ℤ where
  pow x
    n :=
    .mk ((x : 𝕜) ^ n) <| by rw [mem_sphere_zero_iff_norm, norm_zpow, mem_sphere_zero_iff_norm.1 x.coe_prop, one_zpow]

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