Description: The function F enumerates all equivalence classes in Z/nZ for each n . When n = 0 , ZZ / 0 ZZ = ZZ / { 0 } ~ZZ so we let W = ZZ ; otherwise W = { 0 , ... , n - 1 } enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by Mario Carneiro, 2-May-2016) (Revised by AV, 13-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | znf1o.y | |
|
znf1o.b | |
||
znf1o.f | |
||
znf1o.w | |
||
Assertion | znf1o | |