instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc

Mathlib.NumberTheory.FunctionField

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

English

The ring of integers ringOfIntegers Fq F is a Dedekind domain (under separability assumptions).

Русский

Кольцо целых ringOfIntegers F_q F является кольцом Дедекина.

LaTeX

$$$\mathrm{ringOfIntegers}_{F_q}F \text{ is a Dedekind domain.}$$$

Lean4

instance [Algebra.IsSeparable (RatFunc Fq) F] : IsDedekindDomain (ringOfIntegers Fq F) :=
  IsIntegralClosure.isDedekindDomain Fq[X] (RatFunc Fq) F _

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

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

Разделы

Аффилиация

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