:: deftheorem defsgn defines signum REALALG3:def 9 :
for R being ordered Ring
for P being Ordering of R
for a being Element of R holds
( ( a in P \ {(0. R)} implies signum (P,a) = 1 ) & ( a = 0. R implies signum (P,a) = 0 ) & ( not a in P \ {(0. R)} & not a = 0. R implies signum (P,a) = - 1 ) );