degree_hermite

Mathlib.RingTheory.Polynomial.Hermite.Basic

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

← MathLib Explorer

English

The degree of hermite(n) equals n.

Русский

Степень Hermite(n) равна n.

LaTeX

$$$\deg(\operatorname{hermite}(n)) = n$$$

Lean4

@[simp]
theorem degree_hermite (n : ℕ) : (hermite n).degree = n :=
  by
  rw [degree_eq_of_le_of_coeff_ne_zero]
  · simp_rw [degree_le_iff_coeff_zero, Nat.cast_lt]
    rintro m hnm
    exact coeff_hermite_of_lt hnm
  · simp [coeff_hermite_self n]

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

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

Разделы

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

Аффилиация

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