theorem :: UNIROOTS:18

for R being finite Skew-Field holds card (MultGroup R) = (card R) - 1