pow_expChar_pow_inj_of_pNilradical_eq_bot

English

If pNilradical R p = ⊥ for a commutative ring R and ExpChar R p, then for every n, the map x ↦ x^{p^n} is injective on R.

Русский

Если pNilradical R p = ⊥ и характеристика R равна p, тогда для любого n отображение x ↦ x^{p^n} инъективно на R.

LaTeX

$$$$ pNilradical(R,p)=\\bot \\Rightarrow (\\forall n:\\mathbb{N}, \\; \\text{Injective}(x \\mapsto x^{p^{n}})). $$$$

Lean4

theorem pow_expChar_pow_inj_of_pNilradical_eq_bot (R : Type*) [CommRing R] (p : ℕ) [ExpChar R p]
    (h : pNilradical R p = ⊥) (n : ℕ) : Function.Injective fun x : R ↦ x ^ p ^ n := fun _ _ H ↦
  sub_eq_zero.1 <| Ideal.mem_bot.1 <| h ▸ sub_mem_pNilradical_iff_pow_expChar_pow_eq.2 ⟨n, H⟩

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