eq_zero_of_p_mul_eq_zero — Mathlib

English

Let k be a perfect ring of characteristic p. Then the Witt ring 𝕎k has no p-torsion: if x ∈ 𝕎k and x * p = 0, then x = 0.

Русский

Пусть k — совершенное кольцо характерa p. Тогда кольца Witt 𝕎k не содержит p‑торосии: если x ∈ 𝕎k и x · p = 0, то x = 0.

LaTeX

$$$\\forall x \\in 𝕎 k,\\ x \\cdot p = 0 \\Rightarrow x = 0$$$

Lean4

/-- If `k` is a perfect ring of characteristic `p`, then the ring of Witt vectors `𝕎 k` is
`p`-torsion free.
-/
theorem eq_zero_of_p_mul_eq_zero (x : 𝕎 k) (h : x * p = 0) : x = 0 := by
  rwa [← frobenius_verschiebung, map_eq_zero_iff _ (frobenius_bijective p k).injective,
    map_eq_zero_iff _ (verschiebung_injective p k)] at h

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