pow — Mathlib

English

Exponentiation by natural numbers on the nonnegative subtype is defined by lifting the ambient power, preserving nonnegativity.

Русский

Возведение в натуральную степень на подтипе неотрицательных элементов определяется как поднятие степени в окружении и сохраняет неотрицательность.

LaTeX

$$$ (a : { x : \alpha // 0 ≤ x }) ^ n = ⟨a^n, pow\_nonneg a.2 n⟩ $$$

Lean4

instance pow : Pow { x : α // 0 ≤ x } ℕ where pow x n := ⟨(x : α) ^ n, pow_nonneg x.2 n⟩

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