natDegree_preΨ'_le — Mathlib

English

For n ∈ N, the natDegree of W.preΨ' n is at most (n^2 - (4 if n even else 1))/2.

Русский

Для натурального n степерь natDegree полинома W.preΨ' n не превосходит (n^2 - (4, если nчетное, иначе 1))/2.

LaTeX

$$\operatorname{natDegree}(W.preΨ'_n) \le \frac{n^2 - (\text{if } \text{Even}(n) \text{ then } 4 \text{ else } 1)}{2}$$

Lean4

theorem natDegree_preΨ'_le (n : ℕ) : (W.preΨ' n).natDegree ≤ (n ^ 2 - if Even n then 4 else 1) / 2 :=
  (W.natDegree_coeff_preΨ' n).left

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