coeff_p — Mathlib

English

In a Witt vector (p), the coefficient at index i is 1 if i = 1 and 0 otherwise.

Русский

В векторе Витта коэффициент при индексе i равен 1, если i = 1, и 0 в противном случае.

LaTeX

$$[CharP R p] coeff_p : (p : 𝕎 R).coeff i = if i = 1 then 1 else 0$$

Lean4

theorem coeff_p [CharP R p] (i : ℕ) : (p : 𝕎 R).coeff i = if i = 1 then 1 else 0 :=
  by
  split_ifs with hi
  · simpa only [hi, pow_one] using coeff_p_pow p R 1
  · simpa only [pow_one] using coeff_p_pow_eq_zero p R hi

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