Description: The Chinese Remainder Theorem: the function that maps x to its remainder classes mod M and mod N is 1-1 and onto when M and N are coprime. (Contributed by Mario Carneiro, 24-Feb-2014) (Proof shortened by Mario Carneiro, 2-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | crth.1 | |
|
crth.2 | |
||
crth.3 | |
||
crth.4 | |
||
Assertion | crth | |