:: deftheorem Def12 defines ValuatRing FVALUAT1:def 12 :
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
for b₃ being non degenerated strict commutative Ring holds
( b₃ = ValuatRing v iff ( the carrier of b₃ = NonNegElements v & the addF of b₃ = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b₃ = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b₃ = 0. K & the OneF of b₃ = 1. K ) );