English
A truncated Witt vector is simply a function Fin n → R, i.e., the first n coefficients of a Witt vector over R.
Русский
Траunctuation Witt-вектор — это просто отображение Fin n → R, то есть первые n коэффициентов Witt-вектора над R.
LaTeX
$$$\\mathrm{TruncatedWittVector}\\; p\\; n\\; R \\cong (\\mathrm{Fin}\\ n \\to R)$$$
Lean4
/-- A truncated Witt vector over `R` is a vector of elements of `R`,
i.e., the first `n` coefficients of a Witt vector.
We will define operations on this type that are compatible with the (untruncated) Witt
vector operations.
`TruncatedWittVector p n R` takes a parameter `p : ℕ` that is not used in the definition.
In practice, this number `p` is assumed to be a prime number,
and under this assumption we construct a ring structure on `TruncatedWittVector p n R`.
(`TruncatedWittVector p₁ n R` and `TruncatedWittVector p₂ n R` are definitionally
equal as types but will have different ring operations.)
-/
@[nolint unusedArguments]
def TruncatedWittVector (_ : ℕ) (n : ℕ) (R : Type*) :=
Fin n → R
