theorem FAut: :: FIELD_16:65

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
{ f where f is Automorphism of F : verum } = { ((Frob F) `^ m) where m is Nat : ( 0 <= m & m <= n - 1 ) }