for n being non trivial Nat holds Char (Polynom-Ring (Z/ n)) <> 0 ;