peval — Mathlib

English

The Witt vector functor is lawful: the usual functor laws hold for all p.

Русский

Функтор Witt‑векторов удовлетворяет обычным законам функторов для любого p.

LaTeX

$$$\\mathrm{WittVector}_p \\text{ is a LawfulFunctor}$$$

Lean4

/-- An auxiliary definition used in `WittVector.eval`.
Evaluates a polynomial whose variables come from the disjoint union of `k` copies of `ℕ`,
with a curried evaluation `x`.
This can be defined more generally but we use only a specific instance here. -/
def peval {k : ℕ} (φ : MvPolynomial (Fin k × ℕ) ℤ) (x : Fin k → ℕ → R) : R :=
  aeval (Function.uncurry x) φ

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