isAlgebraic_root

Mathlib.RingTheory.AdjoinRoot

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

English

If f is nonzero, then the root of f is algebraic over R.

Русский

Если f ≠ 0, то корень f является алгебраическим над R.

LaTeX

$$$\\text{If } f \\neq 0,\\; \\text{IsAlgebraic}_R(\\mathrm{root}(f)).$$$

Lean4

theorem isAlgebraic_root (hf : f ≠ 0) : IsAlgebraic R (root f) :=
  ⟨f, hf, eval₂_root f⟩

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

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

Разделы

Аффилиация

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