coeff_preΨ' — Mathlib

English

For any W and n ∈ N, the coefficient of W.preΨ' n at the index (n^2 - if Even n then 4 else 1)/2 equals if Even n then n/2 else n.

Русский

Для W и натурального n коэффициент W.preΨ' n при индексе (n^2 - если n чётное, то 4, иначе 1)/2 равен: если n чётное, то n/2, иначе n.

LaTeX

$$ (W.preΨ'_n).coeff\left(\frac{n^2 - \text{if Even}(n) \text{ then } 4 \text{ else } 1}{2}\right) = \begin{cases} \frac{n}{2}, & \text{Even}(n) \\ n, & \text{not Even}(n) \end{cases} $$

Lean4

@[simp]
theorem coeff_preΨ' (n : ℕ) : (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) = if Even n then n / 2 else n :=
  by
  convert (W.natDegree_coeff_preΨ' n).right using 1
  rcases n.even_or_odd' with ⟨n, rfl | rfl⟩ <;> simp [expCoeff, n.not_even_two_mul_add_one]

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