coeff_p_zero — Mathlib

English

Let R be a commutative ring of characteristic p. Then the Witt vector p has zeroth coefficient equal to 0.

Русский

Пусть R — коммутативное кольцо характеристикой p. Тогда Witt-вектор p имеет нулевой коэффициент на позиции 0.

LaTeX

$$$ (p : 𝕎 R).coeff 0 = 0 $$$

Lean4

@[simp]
theorem coeff_p_zero [CharP R p] : (p : 𝕎 R).coeff 0 = 0 :=
  by
  rw [coeff_p, if_neg]
  exact zero_ne_one

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