inftyValuation_apply

Mathlib.NumberTheory.FunctionField

URI: https://scilib.ai/kg/mathlib#FunctionField.inftyValuation_apply

English

The inftyValuation agrees with inftyValuationDef on any x: inftyValuation x = inftyValuationDef x.

Русский

inftyValuation совпадает с inftyValuationDef на любом элементе x.

LaTeX

$$$\text{inftyValuation}(x) = inftyValuationDef(x).$$$

Lean4

theorem inftyValuation_apply {x : RatFunc Fq} : inftyValuation Fq x = inftyValuationDef Fq x :=
  rfl

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

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

Разделы

Аффилиация

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