coeff_preΨ'_ne_zero — Mathlib

English

If (n : R) ≠ 0, then the coefficient of W.preΨ' n at the index (n^2 - if Even n then 4 else 1)/2 is nonzero.

Русский

Если (n : R) ≠ 0, то коэффициент W.preΨ' n при индексе (n^2 - если n четное, то 4, иначе 1)/2 не равен нулю.

LaTeX

$$(n \in R) \neq 0 \Rightarrow (W.preΨ' n).coeff\left(\frac{n^2 - \text{if Even}(n) \text{ then } 4 \text{ else } 1}{2}\right) \neq 0$$

Lean4

theorem coeff_preΨ'_ne_zero {n : ℕ} (h : (n : R) ≠ 0) : (W.preΨ' n).coeff ((n ^ 2 - if Even n then 4 else 1) / 2) ≠ 0 :=
  by
  rcases n.even_or_odd' with ⟨n, rfl | rfl⟩
  · rw [coeff_preΨ', if_pos <| even_two_mul n, n.mul_div_cancel_left two_pos]
    exact right_ne_zero_of_mul <| by rwa [← Nat.cast_mul]
  · rwa [coeff_preΨ', if_neg n.not_even_two_mul_add_one]

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