truncate_lift — Mathlib

English

Given a compatible family of truncated Witt vectors f, one can form a Witt vector by taking the final coefficient from each f k, i.e., liftFun builds a Witt vector from the family.

Русский

Дана совместимая семья тронкатных виттовых векторов f, можно получить виттовектор, взяв последний коэффициент каждого f k; liftFun строит виттовектор из семьи.

LaTeX

$$$$ \\text{liftFun}(s) = \\bigl( \\mathrm{coeff}(\\mathrm{Fin.last}, f(k+1)(s)) \\bigr)_{k\\ge 0}. $$$$

Lean4

@[simp]
theorem truncate_lift (s : S) : WittVector.truncate n (lift _ f_compat s) = f n s :=
  truncate_liftFun _ f_compat s

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