C

Mathlib.NumberTheory.FunctionField

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

English

The valuation of the indeterminate X equals exp(1).

Русский

Валюация переменной X равна exp(1).

LaTeX

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

Lean4

@[simp]
theorem C {k : Fq} (hk : k ≠ 0) : inftyValuation Fq (RatFunc.C k) = 1 := by simp [inftyValuation_apply, hk]

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

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

Разделы

Аффилиация

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