instIsDomain — Mathlib

English

If R is a domain (integral domain) with Char p, then the Witt vectors 𝕎_p(R) form an integral domain.

Русский

Если R — интегральное области с характеристикой p, то Witt-векторы 𝕎_p(R) образуют интегральную область.

LaTeX

$$$\text{If } R \text{ is an integral domain and } \operatorname{Char}(R) = p, \; \mathbb{W}_p(R) \text{ is an integral domain.}$$$

Lean4

instance instIsDomain [CharP R p] [IsDomain R] : IsDomain (𝕎 R) :=
  NoZeroDivisors.to_isDomain _

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