theorem Lm0: :: FIELD_15:35

for p being Prime
for R being commutative b₁ -characteristic Ring
for a being Element of R holds p * a = 0. R