isIntegral_root

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.isIntegral_root

English

If f ≠ 0 in K[X], then the root of f is integral over K.

Русский

Если f ≠ 0 в K[X], корень f интегрирован над K.

LaTeX

$$IsIntegral(K, root f) for f ≠ 0$$

Lean4

theorem isIntegral_root (hf : f ≠ 0) : IsIntegral K (root f) :=
  (isAlgebraic_root hf).isIntegral

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

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

Разделы

Аффилиация

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