isMonicOfDegree_X_add_one

Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

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

English

For any ring R, X + C r is monic of degree 1 for any r ∈ R.

Русский

Для любого кольца R полином X + C r мономичен степени 1 для любого r ∈ R.

LaTeX

$$$IsMonicOfDegree(X + C r, 1)$$$

Lean4

theorem isMonicOfDegree_X_add_one (r : R) : IsMonicOfDegree (X + C r) 1 :=
  (isMonicOfDegree_X R).add_right (by rw [natDegree_C]; exact zero_lt_one)

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

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

Разделы

Аффилиация

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