def

Mathlib.NumberTheory.FunctionField

URI: https://scilib.ai/kg/mathlib#FunctionField.inftyValuedFqt.def

English

The valuation on RatFunc Fq is defined by inftyValuationDef and agrees with inftyValuation.

Русский

Валюация на RatFunc F_q задается через inftyValuationDef и совпадает с inftyValuation.

LaTeX

$$$\text{inftyValuation} = \mathrm{inftyValuationDef}.$$$

Lean4

theorem «def» {x : RatFunc Fq} : (inftyValuedFqt Fq).v x = inftyValuationDef Fq x :=
  rfl

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

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

Разделы

Аффилиация

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