zpow — Mathlib

English

There is a defined power operation of NNReal by integers: x^n is nonnegative for all integers n.

Русский

Существует операция степеней для NNReal на целые числа: x^n неотрицательно для всех целых n.

LaTeX

$$$ zpow: \\mathbb{R}_{\\ge 0}^{\\mathbb{Z}} \\\\; (x,n) \\mapsto x^{n} \\text{ with } zpow\\_nonneg \\text{ proof}$$$

Lean4

noncomputable instance zpow : Pow ℝ≥0 ℤ where pow x n := ⟨(x : ℝ) ^ n, zpow_nonneg x.2 _⟩

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