:: deftheorem Def4 defines CR_coefficients INT_6:def 4 :
for m being CR_Sequence
for b₂ being FinSequence holds
( b₂ is CR_coefficients of m iff ( len b₂ = len m & ( for i being Nat st i in dom b₂ holds
ex s, mm being Integer st
( mm = (Product m) / (m . i) & s * mm,1 are_congruent_mod m . i & b₂ . i = s * ((Product m) / (m . i)) ) ) ) );