theorem Th103: :: MATGRP_0:90
for R being Ring
for n being Nat
for A being Matrix of n,R st ( for B being Matrix of n,R holds A * B = B * A ) holds
ex z being Element of R st
( z in center R & A = z * (1. (R,n)) )