leadingCoeff_X_pow

Mathlib.Algebra.Polynomial.Degree.Definitions

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

English

If you update the n-th coefficient of p by a, the degree is at most max(degree p, n).

Русский

Если обновить n-й коэффициент p на a, степень ≤ max(deg p, n).

LaTeX

$$$\deg(p.update(n, a)) \le \max(\deg(p), n)$$$

Lean4

theorem leadingCoeff_X_pow (n : ℕ) : leadingCoeff ((X : R[X]) ^ n) = 1 := by
  simpa only [C_1, one_mul] using leadingCoeff_C_mul_X_pow (1 : R) n

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

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

Разделы

Аффилиация

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