let R be finite Skew-Field; :: thesis: for s being Element of R
for t being Element of (MultGroup R) st t = s holds
card (Centralizer t) = (card the carrier of (centralizer s)) - 1
let s be Element of R; :: thesis: for t being Element of (MultGroup R) st t = s holds
card (Centralizer t) = (card the carrier of (centralizer s)) - 1
let t be Element of (MultGroup R); :: thesis: ( t = s implies card (Centralizer t) = (card the carrier of (centralizer s)) - 1 )
assume A1: t = s ; :: thesis: card (Centralizer t) = (card the carrier of (centralizer s)) - 1
set ct = Centralizer t;
set cs = centralizer s;
set cct = the carrier of (Centralizer t);
set ccs = the carrier of (centralizer s);
the carrier of (MultGroup R) = NonZero R by UNIROOTS:def 1;
then not 0. R in the carrier of (MultGroup R) by ZFMISC_1:56;
then not 0. R in MultGroup R ;
then not 0. R in Centralizer t by Th7;
then A2: not 0. R in the carrier of (Centralizer t) ;
the carrier of (Centralizer t) \/ {(0. R)} = the carrier of (centralizer s) by A1, Th29;
then card the carrier of (centralizer s) = (card the carrier of (Centralizer t)) + 1 by A2, CARD_2:41;
hence card (Centralizer t) = (card the carrier of (centralizer s)) - 1 ; :: thesis: verum