isIntegral_root

Mathlib.RingTheory.IsAdjoinRoot

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

English

root is integral over R: there exists a monic polynomial f with root as a root.

Русский

корень целостен над R: существует моноичный многочлен f, корень которого является корнем.

LaTeX

$$$ IsIntegral R h.root $$$

Lean4

theorem isIntegral_root : IsIntegral R h.root :=
  ⟨f, h.monic, h.aeval_root_self⟩

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

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

Разделы

Аффилиация

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