coeff_hermite_of_lt — Mathlib

English

If n < k, then the coefficient of hermite(n) at k is zero.

Русский

Если n < k, то коэффициент Hermite(n) в степени k равен нулю.

LaTeX

$$$n < k \Rightarrow \operatorname{coeff}(\operatorname{hermite}(n),k) = 0$$$

Lean4

theorem coeff_hermite_of_lt {n k : ℕ} (hnk : n < k) : coeff (hermite n) k = 0 :=
  by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hnk
  clear hnk
  induction n generalizing k with
  | zero => exact coeff_C
  | succ n ih =>
    have : n + k + 1 + 2 = n + (k + 2) + 1 := by ring
    rw [coeff_hermite_succ_succ, add_right_comm, this, ih k, ih (k + 2), mul_zero, sub_zero]

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