zpow — Mathlib

English

Integer powers are defined on the nonnegative subtype: a^n ∈ { x ≥ 0 } for a ∈ { x ≥ 0 } and n ∈ ℤ.

Русский

Целочисленные степени определены на неотрицательном подмножество: a^n ∈ { x ≥ 0 } для a ∈ { x ≥ 0 } и n ∈ ℤ.

LaTeX

$$$\\text{zpow} : \\text{Pow}({ x : α // 0 ≤ x } , \\mathbb{Z})$ with $ (a)^n = ⟨(a : α)^n, zpow\\_nonneg(a.2, n)⟩$$$

Lean4

instance zpow : Pow { x : α // 0 ≤ x } ℤ :=
  ⟨fun a n => ⟨(a : α) ^ n, zpow_nonneg a.2 _⟩⟩

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