sub_mem_pNilradical_iff_pow_expChar_pow_eq

English

In a commutative ring R of characteristic p, for x,y ∈ R, x − y ∈ pNilradical R p iff ∃ n with x^{p^n} = y^{p^n}.

Русский

В коммутативном кольце R характеристика p: x−y ∈ pNilradical R p тогда и только тогда, когда ∃ n: x^{p^n} = y^{p^n}.

LaTeX

$$$$ x-y \\in pNilradical(R,p) \\iff \\exists n:\\mathbb{N}, \\; x^{p^{n}} = y^{p^{n}}. $$$$

Lean4

theorem sub_mem_pNilradical_iff_pow_expChar_pow_eq {R : Type*} [CommRing R] {p : ℕ} [ExpChar R p] {x y : R} :
    x - y ∈ pNilradical R p ↔ ∃ n : ℕ, x ^ p ^ n = y ^ p ^ n := by
  simp_rw [mem_pNilradical, sub_pow_expChar_pow, sub_eq_zero]

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