:: deftheorem defFr defines FrobeniusMorphism FIELD_16:def 6 :
for R being Ring
for b₂ being Function of R,R holds
( b₂ = FrobeniusMorphism R iff for a being Element of R holds b₂ . a = a |^ (Char R) );