for p being Prime
for F being Field holds
( Char F = p iff PrimeField F, Z/ p are_isomorphic )