isMonicOfDegree_X_sub_one

Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

URI: https://scilib.ai/kg/mathlib#Polynomial.isMonicOfDegree_X_sub_one

English

For any r in R, the polynomial X − C r is monic of degree 1.

Русский

Для любого r в R многочлен X − C r моноичен степени 1.

LaTeX

$$$\\text{IsMonicOfDegree}(X - C r, 1)$$$

Lean4

theorem isMonicOfDegree_X_sub_one (r : R) : IsMonicOfDegree (X - C r) 1 :=
  (isMonicOfDegree_X R).sub (by rw [natDegree_C]; exact zero_lt_one)

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

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

Разделы

Аффилиация

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