coeff_hermite_self

Mathlib.RingTheory.Polynomial.Hermite.Basic

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

← MathLib Explorer

English

For all n, the coefficient of hermite(n) at position n is 1.

Русский

Для всех n коэффициент Hermite(n) при позиции n равен 1.

LaTeX

$$$\operatorname{coeff}(\operatorname{hermite}(n),n)=1$$$

Lean4

@[simp]
theorem coeff_hermite_self (n : ℕ) : coeff (hermite n) n = 1 := by
  induction n with
  | zero => exact coeff_C
  | succ n ih =>
    rw [coeff_hermite_succ_succ, ih, coeff_hermite_of_lt, mul_zero, sub_zero]
    simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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