Frobenius endomorphism

Let $𝐾$ be a field of prime characteristic $𝑝$ . The Frobenius endomorphism $𝜎 : 𝐾 \to 𝐾$ is defined by #m/def/field

𝜎 (𝑥) = 𝑥 𝑝

which is indeed an endomorphism by the Freshman's dream. This is surjective, and thus a Frobenius automorphism, precisely when $𝐾$ is a Perfect field.

#state/tidy | #lang/en | #SemBr