p_nonzero — Mathlib

English

In a nontrivial commutative ring R of characteristic p, the Witt vector p is nonzero: (p : 𝕎 R) ≠ 0.

Русский

В не тривиальном коммутативном кольце R характеристикой p Witt-вектор p не нулевой: (p : 𝕎 R) ≠ 0.

LaTeX

$$$ (p : 𝕎 R) \neq 0 $$$

Lean4

theorem p_nonzero [Nontrivial R] [CharP R p] : (p : 𝕎 R) ≠ 0 :=
  by
  intro h
  simpa only [h, zero_coeff, zero_ne_one] using coeff_p_one p R

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