frobenius_inj — Mathlib

English

Let R be a commutative ring with ExpChar R p. Then the Frobenius endomorphism is injective.

Русский

Пусть R — коммутативное кольцо с характеристикой p. Тогда Фробениус-преобразование инъективно.

LaTeX

$$$\\forall x,y\\in R,\\ x^p = y^p \\Rightarrow x = y$$$

Lean4

theorem frobenius_inj : Function.Injective (frobenius R p) :=
  iterateFrobenius_one (R := R) p ▸ iterateFrobenius_inj R p 1

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