for R being Ring holds Char (Polynom-Ring R) = Char R by RING_3:88;