ne_zero_of_finite

Mathlib.FieldTheory.Minpoly.Field

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

English

If p ≠ 0 and x is a root of p, then deg(minpoly A x) ≤ deg p.

Русский

Если p ≠ 0 и x является корнем p, то deg(minpoly A x) ≤ deg p.

LaTeX

$$$\\deg(\\minpoly A x) \\le \\deg p \\quad \\text{whenever } p \\neq 0 \\text{ and } aeval\ x\ p = 0$$$

Lean4

theorem ne_zero_of_finite (e : B) [FiniteDimensional A B] : minpoly A e ≠ 0 :=
  minpoly.ne_zero <| .of_finite A _

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

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

Разделы

Аффилиация

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