:: deftheorem defines #Q PREPOWER:def 4 :
for a being Real
for p being Rational holds a #Q p = (denominator p) -Root (a #Z (numerator p));