leadingCoeff_X_pow_add_one

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

The leading coefficient of X^n + 1 is 1 for any n > 0.

Русский

Для любого n > 0 ведущий коэффициент X^n + 1 равен 1.

LaTeX

$$$ (X^n + 1).leadingCoeff = 1 $ with $0 < n$$$

Lean4

@[simp]
theorem leadingCoeff_X_pow_add_one {n : ℕ} (hn : 0 < n) : (X ^ n + 1 : R[X]).leadingCoeff = 1 :=
  leadingCoeff_X_pow_add_C hn

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

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

Разделы

Аффилиация

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