eq_X_sub_C'

Mathlib.FieldTheory.Minpoly.Field

URI: https://scilib.ai/kg/mathlib#minpoly.eq_X_sub_C'

English

For any a in A, the minimal polynomial of a is X − C a.

Русский

Для любого a ∈ A минимальный полином a равен X − C a.

LaTeX

$$$\minpoly_A(a) = X - C a$$$

Lean4

theorem eq_X_sub_C' (a : A) : minpoly A a = X - C a :=
  eq_X_sub_C A a

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

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

Разделы

Аффилиация

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