p_nonzero — Mathlib

English

In the fraction ring of Witt vectors, the element p is nonzero: (p : FractionRing (𝕎 R)) ≠ 0.

Русский

Во FractionRing Witt-векторов элемент p не равен нулю: (p : FractionRing (𝕎 R)) ≠ 0.

LaTeX

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

Lean4

theorem p_nonzero [Nontrivial R] [CharP R p] : (p : FractionRing (𝕎 R)) ≠ 0 := by
  simpa using (IsFractionRing.injective (𝕎 R) (FractionRing (𝕎 R))).ne (WittVector.p_nonzero _ _)

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