frobeniusPolyAux — Mathlib

English

The auxiliary polynomial frobeniusPolyAux(p,n) is a polynomial in the ring of integers, constructed so that frobeniusPoly(p,n) = X_{n+1} − sum of a finite combination of lower indexed terms involving frobeniusPolyAux(p,i).

Русский

Вспомогательный многочлен frobeniusPolyAux(p,n) строится так, что frobeniusPoly(p,n) выражается через X_{n+1} минус конечная сумма нижеиндексированных слагаемых, содержащих frobeniusPolyAux(p,i).

LaTeX

$$$\forall p,n,\; frobeniusPolyAux(p,n) = X(n+1) - \sum_{i

Lean4

/-- An auxiliary polynomial over the integers, that satisfies
`p * (frobeniusPolyAux p n) + X n ^ p = frobeniusPoly p n`.
This makes it easy to show that `frobeniusPoly p n` is congruent to `X n ^ p`
modulo `p`. -/
noncomputable def frobeniusPolyAux : ℕ → MvPolynomial ℕ ℤ
  | n =>
    X (n + 1) -
      ∑ i : Fin n,
        have _ := i.is_lt
        ∑ j ∈ range (p ^ (n - i)),
          (((X (i : ℕ) ^ p) ^ (p ^ (n - (i : ℕ)) - (j + 1)) : MvPolynomial ℕ ℤ) * (frobeniusPolyAux i) ^ (j + 1)) *
            C (((p ^ (n - i)).choose (j + 1) / (p ^ (n - i - v p (j + 1))) * ↑p ^ (j - v p (j + 1)) : ℕ) : ℤ)

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