leadingCoeff_hermite

Mathlib.RingTheory.Polynomial.Hermite.Basic

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

English

The leading coefficient of hermite(n) is 1.

Русский

Ведущий коэффициент Hermite(n) равен 1.

LaTeX

$$$\text{leadingCoeff}(\operatorname{hermite}(n)) = 1$$$

Lean4

@[simp]
theorem leadingCoeff_hermite (n : ℕ) : (hermite n).leadingCoeff = 1 := by
  rw [← coeff_natDegree, natDegree_hermite, coeff_hermite_self]

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

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

Разделы

Аффилиация

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