instIsDomainSubtypeMemSubalgebraPolynomial

Mathlib.NumberTheory.FunctionField

URI: https://scilib.ai/kg/mathlib#FunctionField.ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial

English

The ring of integers associated to the function field, denoted ringOfIntegers Fq F, is an integral domain.

Русский

Кольцо целых кольца функции ringOfIntegers Fq F является интегральным доменом.

LaTeX

$$$\mathrm{ringOfIntegers}_{F_q}F \text{ is an integral domain.}$$$

Lean4

instance : IsDomain (ringOfIntegers Fq F) :=
  (ringOfIntegers Fq F).isDomain

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

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

Разделы

Аффилиация

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