instFieldFqtInfty

Mathlib.NumberTheory.FunctionField

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

English

The field structure on FqtInfty Fq is established by a field instance built from the completion.

Русский

Поле FqtInfty Fq имеет инстанс поля, полученный из завершения.

LaTeX

$$$\operatorname{Field}(\mathrm{FqtInfty}_{F_q})$$$

Lean4

instance : Field (FqtInfty Fq) :=
  letI := inftyValuedFqt Fq
  UniformSpace.Completion.instField

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

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

Разделы

Аффилиация

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