English
For any W over a commutative ring R and any nonzero n in R, natDegree of W.preΨ' n equals (n^2 - if Even n then 4 else 1)/2.
Русский
Для любой W над кольцом R и любого n с n ≠ 0, natDegree(W.preΨ' n) = (n^2 - if Even n then 4 else 1)/2.
LaTeX
$$natDegree(W.preΨ'(n)) = \frac{n^2 - \text{if Even}(n) \text{ then } 4 \text{ else } 1}{2}$$
Lean4
theorem natDegree_preΨ_pos {n : ℤ} (hn : 2 < n.natAbs) (h : (n : R) ≠ 0) : 0 < (W.preΨ n).natDegree := by
induction n using Int.negInduction with
| nat n => simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
| neg ih n =>
simpa only [preΨ_neg, natDegree_neg] using ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h