natDegree_preΨ_pos — Mathlib

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

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