mk — Mathlib · SciLib

English

Construct a Witt vector from a sequence of ring elements: the nth coefficient of 𝕎 p R is the nth term of the input sequence.

Русский

Построим Witt‑вектор из последовательности элементов кольца: n‑й коэффициент 𝕎 p R равен n‑му члену входной последовательности.

LaTeX

$$$(\mathrm{WittVector.mk}(p, x)).\\mathrm{coeff}(n) = x(n)$$$

Lean4

/-- Construct a Witt vector `mk p x : 𝕎 R` from a sequence `x` of elements of `R`.

This is preferred over `WittVector.mk'` because it has `p` explicit.
-/
def mk (p : ℕ) {R : Type*} (coeff : ℕ → R) : WittVector p R :=
  mk' coeff

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