polyOfInterest — Mathlib

English

Define a polynomial whose degree will be studied; it combines Witt multiplications and Witt polynomials with variable renaming.

Русский

Определим полином, чья степень будет изучаться; он сочетает умножение Witt и Witt-полиномов с переименованием переменных.

LaTeX

$$$\text{polyOfInterest}(p,n) := wittMul(p,n+1) + p^{n+1}X(0,n+1)X(1,n+1) - X(0,n+1)\ rename(...) - X(1,n+1)\rename(...).$$$

Lean4

/-- This is the polynomial whose degree we want to get a handle on. -/
def polyOfInterest (n : ℕ) : 𝕄 :=
  wittMul p (n + 1) + (p : 𝕄) ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
      X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) -
    X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1))

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