ne_zero_iff

Mathlib.FieldTheory.Minpoly.Basic

URI: https://scilib.ai/kg/mathlib#minpoly.ne_zero_iff

English

For nontrivial A, minpoly_A(x) ≠ 0 if and only if x is integral over A.

Русский

Для непустой A minpoly_A(x) ≠ 0 тогда и только тогда, когда x интегрирован над A.

LaTeX

$$$\\minpoly_{A}(x) \\neq 0 \\iff IsIntegral_{A}(x).$$$

Lean4

theorem ne_zero_iff [Nontrivial A] : minpoly A x ≠ 0 ↔ IsIntegral A x :=
  ⟨fun h => of_not_not <| eq_zero.mt h, ne_zero⟩

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

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

Разделы

Аффилиация

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