instNoZeroDivisorsOfCharP — Mathlib

English

If R has characteristic p and is a domain (i.e., has no zero divisors), then the Witt vectors 𝕎_p(R) also have no zero divisors.

Русский

Если R имеет характеристику p и является областью, то 𝕎_p(R) тоже не содержит делителей нуля.

LaTeX

$$$\text{If } \operatorname{Char}(R) = p \text{ and } \mathrm{NoZeroDivisors}(R), \; \mathrm{NoZeroDivisors}(\mathbb{W}_p(R)).$$$

Lean4

instance [CharP R p] [NoZeroDivisors R] : NoZeroDivisors (𝕎 R) :=
  ⟨fun {x y} => by
    contrapose!
    rintro ⟨ha, hb⟩
    rcases verschiebung_nonzero ha with ⟨na, wa, hwa0, rfl⟩
    rcases verschiebung_nonzero hb with ⟨nb, wb, hwb0, rfl⟩
    refine ne_of_apply_ne (fun x => x.coeff (na + nb)) ?_
    dsimp only
    rw [iterate_verschiebung_mul_coeff, zero_coeff]
    exact mul_ne_zero (pow_ne_zero _ hwa0) (pow_ne_zero _ hwb0)⟩

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