theorem FrK: :: FIELD_16:21

for n being Nat
for R being b₁ -characteristic Ring holds ker (Frob R) = { a where a is Element of R : a |^ n = 0. R }