English
If n+k is even, then coeff(hermite n) k equals a product (-1)^((n-k)/2) (n-k-1)‼ times binomial n choose k; otherwise it is zero.
Русский
Если n+k чётно, коэффициент coeff(hermite n) k равен (-1)^((n-k)/2) (n-k-1)‼ · C(n,k); иначе 0.
LaTeX
$$$\text{If }\operatorname{Even}(n+k)\text{, then } \operatorname{coeff}(\operatorname{hermite}(n),k) = (-1)^{(n-k)/2} (n-k-1)‼ \cdot \binom{n}{k},\; \text{else } 0.$$$
Lean4
theorem coeff_hermite_of_even_add {n k : ℕ} (hnk : Even (n + k)) :
coeff (hermite n) k = (-1) ^ ((n - k) / 2) * (n - k - 1)‼ * Nat.choose n k :=
by
rcases le_or_gt k n with h_le | h_lt
· rw [Nat.even_add, ← Nat.even_sub h_le] at hnk
obtain ⟨m, hm⟩ := hnk
rw [(by cutsat : n = 2 * m + k), Nat.add_sub_cancel, Nat.mul_div_cancel_left _ (Nat.succ_pos 1),
coeff_hermite_explicit]
· simp [Nat.choose_eq_zero_of_lt h_lt, coeff_hermite_of_lt h_lt]
