Theorems · Definition · number theory

FiniteField.frobeniusAlgHom

(K : Type u_1) →
  (R : Type u_2) → [inst : Field K] → [Fintype K] → [inst_2 : CommRing R] → [inst_3 : Algebra K R] → R →ₐ[K] R

If R is an algebra over a finite field K, the Frobenius K-algebra endomorphism of R is given by raising every element of R to its #K-th power.

Defined in

Mathlib.FieldTheory.Finite.Basic

Cited by

8 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFintypeCommRingAlgebra