:: deftheorem defines Roots FIELD_4:def 4 :
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R) holds Roots (S,p) = { a where a is Element of S : a is_a_root_of p,S } ;