coeff_ΨSq — Mathlib

English

The coefficient of (W.ΨSq n) at degree n.natAbs^2 − 1 equals n^2.

Русский

Коэффициент полиномa (W.ΨSq n) при степени n^2 − 1 равен n^2.

LaTeX

$$(W.ΨSq n).coeff(n.natAbs^2 - 1) = n^2$$

Lean4

@[simp]
theorem coeff_ΨSq (n : ℤ) : (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = n ^ 2 := by
  induction n using Int.negInduction with
  | nat n => exact_mod_cast (W.natDegree_coeff_ΨSq_ofNat n).right
  | neg ih => rw [ΨSq_neg, Int.natAbs_neg, ← Int.cast_pow, neg_sq, Int.cast_pow, ih]

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