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

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