instZPow

Mathlib.Algebra.Field.Rat

URI: https://scilib.ai/kg/mathlib#NNRat.instZPow

English

There is a power operation Pow ℚ≥0 ℤ, i.e., exponentiation of nonnegative rationals by integers.

Русский

Существуют операции возведения в степень на ℚ≥0 с целыми степенями.

LaTeX

$$$\text{Pow}\ \mathbb{Q}_{\ge 0} \mathbb{Z}$$$

Lean4

instance instZPow : Pow ℚ≥0 ℤ where pow x n := ⟨x ^ n, Rat.zpow_nonneg x.2⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru