instIsFractionRingSubtypeMemSubalgebraPolynomial

Mathlib.NumberTheory.FunctionField

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

English

F is the fraction field of the ringOfIntegers Fq F.

Русский

F является полем дробей кольца целых ringOfIntegers Fq F.

LaTeX

$$$\operatorname{Frac}(\mathrm{ringOfIntegers}_{F_q}F) = F.$$$

Lean4

instance : IsFractionRing (ringOfIntegers Fq F) F :=
  integralClosure.isFractionRing_of_finite_extension (RatFunc Fq) F

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

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

Разделы

Аффилиация

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