isIntegral_root'

Mathlib.RingTheory.AdjoinRoot

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

English

If g is monic in K[X], then root g is integral over K.

Русский

Если g моническое, то корень g интегрален над K.

LaTeX

$$IsIntegral(K, root g) when g is Monic$$

Lean4

theorem isIntegral_root' (hg : g.Monic) : IsIntegral R (root g) :=
  ⟨g, hg, eval₂_root g⟩

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

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

Разделы

Аффилиация

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