degree_X_sub_C

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

If deg p ≤ 1, then p can be written as (C (p.leadingCoeff)) X + C (p.coeff 0).

Русский

Если deg p ≤ 1, то p имеет вид (C (p.leadingCoeff)) X + C (p.coeff 0).

LaTeX

$$$\text{If } \deg(p) \le 1:\; p = C(p_{1})\,X + C(p_{0})$ where $p_{1}=\operatorname{leadingCoeff}(p),\; p_{0}=p(0).$$$

Lean4

@[simp]
theorem degree_X_sub_C (a : R) : degree (X - C a) = 1 := by rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]

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

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

Разделы

Аффилиация

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