leadingCoeff_mul_X_pow

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

Multiplying a polynomial by X^n does not change its leading coefficient.

Русский

Умножение многочлена на X^n не изменяет его ведущую коэффициент.

LaTeX

$$$ \operatorname{leadingCoeff}(p \cdot X^{n}) = \operatorname{leadingCoeff}(p).$$$

Lean4

@[simp]
theorem leadingCoeff_mul_X_pow {p : R[X]} {n : ℕ} : leadingCoeff (p * X ^ n) = leadingCoeff p :=
  leadingCoeff_mul_monic (monic_X_pow n)

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

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

Разделы

Аффилиация

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