:: deftheorem defines [/] RINGFRAC:def 7 :
for R being commutative Ring
for u, v being Element of R holds u [/] v = u * (recip u);