theorem lemex: :: FIELD_16:53

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = p |^ n