:: deftheorem defines dl. SCMRING3:def 1 :
for R being Ring
for k being Nat holds dl. (R,k) = dl. k;