instPowSubtypeLtOfNatInt_mathlib — Mathlib

English

There is a ℤ-action by exponentiation on the positive subtype; for x ∈ {x>0} and n ∈ ℤ, x^n is defined as in the ambient field and remains positive.

Русский

Существует действие ℤ на подпредельном множестве {x>0} через возведение в степень; для x>0 и n∈ℤ x^n определяется как в поле и остаётся положительным.

LaTeX

$$$\\forall x\\in\\{x>0\\},\\ \\forall n\\in\\mathbb{Z},\\ x^n>0.$$$

Lean4

instance : Pow { x : K // 0 < x } ℤ :=
  ⟨fun x n => ⟨(x : K) ^ n, zpow_pos x.2 _⟩⟩

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