degree_mul_X

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

For any polynomial p, deg(p · X) = deg p + 1.

Русский

Для любого многочлена p, deg(p · X) = deg p + 1.

LaTeX

$$$ \deg(p \cdot X) = \deg(p) + 1. $$$

Lean4

@[simp]
theorem degree_mul_X : degree (p * X) = degree p + 1 := by simp [monic_X.degree_mul]

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

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

Разделы

Аффилиация

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