coe_zpow

Mathlib.Algebra.Order.Positive.Field

URI: https://scilib.ai/kg/mathlib#Positive.coe_zpow

English

For x ∈ {x>0} and n ∈ ℤ, the coerced value of x^n equals x^n in K: ↑(x^n) = x^n.

Русский

Для x>0 и n∈ℤ отображение x^n в K совпадает с x^n в K: ↑(x^n) = x^n.

LaTeX

$$$\\uparrow (x^n) = x^n.$$$

Lean4

@[simp]
theorem coe_zpow (x : { x : K // 0 < x }) (n : ℤ) : ↑(x ^ n) = (x : K) ^ n :=
  rfl

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

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

Разделы

Аффилиация

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