coeff_zero — Mathlib

English

For any i ∈ Fin n, the i-th coefficient of the zero truncated Witt vector is 0.

Русский

Для любого i ∈ Fin n i-й коэффициент нулевого обрезанного виттового вектора равен 0.

LaTeX

$$$ (0 : \mathrm{TruncatedWittVector}(p,n,R)).\mathrm{coeff} i = 0 \quad \text{for } i : \mathrm{Fin}(n) $$$

Lean4

@[simp]
theorem coeff_zero (i : Fin n) : (0 : TruncatedWittVector p n R).coeff i = 0 :=
  by
  change coeff i (truncateFun _ 0 : TruncatedWittVector p n R) = 0
  rw [coeff_truncateFun, WittVector.zero_coeff]

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