:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :
for R being Skew-Field
for s being Element of R
for b₃ being strict Skew-Field holds
( b₃ = centralizer s iff ( the carrier of b₃ = { x where x is Element of R : x * s = s * x } & the addF of b₃ = the addF of R || the carrier of b₃ & the multF of b₃ = the multF of R || the carrier of b₃ & 0. b₃ = 0. R & 1. b₃ = 1. R ) );