theorem :: GR_CY_3:36

for p being Prime holds Z/Z* p = MultGroup (INT.Ring p)