X_zpow

Mathlib.NumberTheory.FunctionField

URI: https://scilib.ai/kg/mathlib#FunctionField.inftyValuation.X_zpow

English

The valuation of 1/X equals exp(-1).

Русский

Валюация 1/X равна exp(-1).

LaTeX

$$$\infty\text{-Valuation}(1/ X) = \exp(-1).$$$

Lean4

theorem X_zpow (m : ℤ) : inftyValuation Fq (RatFunc.X ^ m) = exp m := by simp

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

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

Разделы

Аффилиация

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