not_isField

Mathlib.NumberTheory.FunctionField

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

← MathLib Explorer

English

The ring of integers ringOfIntegers Fq F is not a field.

Русский

Кольцо целых ringOfIntegers Fq F не является полем.

LaTeX

$$$\mathrm{ringOfIntegers}_{F_q}F \text{ is not a field.}$$$

Lean4

theorem not_isField : ¬IsField (ringOfIntegers Fq F) := by
  simpa [← (IsIntegralClosure.isIntegral_algebra Fq[X] F).isField_iff_isField (algebraMap_injective Fq F)] using
    Polynomial.not_isField Fq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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