theorem Th39: :: MATRIX14:39

for n being Element of NAT
for K being Field
for A being Matrix of n,K st n > 0 & A * (1,1) <> 0. K holds
ex P being Matrix of n,K st
( P is invertible & (A * P) * (1,1) = 1. K & ( for j being Element of NAT st 1 < j & j <= n holds
(A * P) * (1,j) = 0. K ) & ( for i being Element of NAT st 1 < i & i <= n & A * (i,1) = 0. K holds
(A * P) * (i,1) = 0. K ) )