coeff_hermite_succ_zero — Mathlib

English

The constant term of the next Hermite is the negative of the coefficient of X in the current one.

Русский

Постоянный член следующего полинома Эрмита равен минусу коэффициента перед X в текущем полиномe.

LaTeX

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

Lean4

theorem coeff_hermite_succ_zero (n : ℕ) : coeff (hermite (n + 1)) 0 = -coeff (hermite n) 1 := by simp [coeff_derivative]

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