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 - if Even n then 4 else 1)/2) не равен нулю.

LaTeX

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

Lean4

theorem coeff_preΨ_ne_zero {n : ℤ} (h : (n : R) ≠ 0) :
    (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) ≠ 0 := by
  induction n using Int.negInduction with
  | nat n => simpa only [preΨ_ofNat, Int.even_coe_nat] using W.coeff_preΨ'_ne_zero <| by exact_mod_cast h
  | neg ih n =>
    simpa only [preΨ_neg, coeff_neg, neg_ne_zero, Int.natAbs_neg, even_neg] using
      ih n <| neg_ne_zero.mp <| by exact_mod_cast h

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