unitsMap_val
shows that coercing from (ZMod m)ˣ
to ZMod n
gives the same result
when going via (ZMod n)ˣ
and ZMod m
.
unitsMap_val
shows that coercing from (ZMod m)ˣ
to ZMod n
gives the same result
when going via (ZMod n)ˣ
and ZMod m
.