leadingCoeff_pow_X_add_C

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

For every r and i, the leading coefficient of (X + C(r))^i is 1.

Русский

Для любого r и i ведущий коэффициент (X + C(r))^i равен 1.

LaTeX

$$$\operatorname{leadingCoeff}\left(\left(X + C r\right)^i\right) = 1$$$

Lean4

@[simp]
theorem leadingCoeff_pow_X_add_C (r : R) (i : ℕ) : leadingCoeff ((X + C r) ^ i) = 1 :=
  by
  nontriviality
  rw [leadingCoeff_pow'] <;> simp

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

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

Разделы

Аффилиация

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