natDegree_ΨSq_le — Mathlib

English

For any integer n, the natDegree of W.ΨSq n is at most n.natAbs^2 − 1.

Русский

Для любого целого n, natDegree(W.ΨSq n) не превышает n^2 − 1 (с natAbs).

LaTeX

$$(W.ΨSq n).natDegree ≤ n.natAbs^2 - 1$$

Lean4

theorem natDegree_ΨSq_le (n : ℤ) : (W.ΨSq n).natDegree ≤ n.natAbs ^ 2 - 1 := by
  induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_ΨSq_ofNat n).left
  | neg ih => simp_rw [ΨSq_neg, Int.natAbs_neg, ih]

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