let n be Nat; :: thesis: for K being Field
for L being Element of K holds
( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) )
let K be Field; :: thesis: for L being Element of K holds
( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) )
let L be Element of K; :: thesis: ( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) )
set B = Jordan_block (L,n);
A1: ( not Jordan_block (L,n) is invertible or L <> 0. K or n = 0 )

proof

assume Jordan_block (L,n) is invertible ; :: thesis: ( L <> 0. K or n = 0 )
then Det (Jordan_block (L,n)) is unital by LAPLACE:34;
then not Det (Jordan_block (L,n)) is zero by LAPLACE:42, LAPLACE:43;
then A2: Det (Jordan_block (L,n)) <> 0. K ;
assume A3: L = 0. K ; :: thesis: n = 0
assume n <> 0 ; :: thesis: contradiction
then A4: n in Seg n by FINSEQ_1:3;
then ( dom (n |-> L) = Seg n & (n |-> L) . n = L ) by FINSEQ_2:57, FINSEQ_2:124;
then 0. K = Product (n |-> L) by A3, A4, FVSUM_1:82
.= (power K) . (L,n) by MATRIXJ1:5 ;
hence contradiction by A2, Th2; :: thesis: verum

end;

( ( n = 0 or L <> 0. K ) implies Jordan_block (L,n) is invertible )

proof

assume A5: ( n = 0 or L <> 0. K ) ; :: thesis: Jordan_block (L,n) is invertible
assume not Jordan_block (L,n) is invertible ; :: thesis: contradiction
then not Det (Jordan_block (L,n)) is unital by LAPLACE:34;
then Det (Jordan_block (L,n)) is zero ;
then 0. K = Det (Jordan_block (L,n))
.= (power K) . (L,n) by Th2
.= Product (n |-> L) by MATRIXJ1:5 ;
then A6: ex k being Nat st
( k in dom (n |-> L) & (n |-> L) . k = 0. K ) by FVSUM_1:82;
dom (n |-> L) = Seg n by FINSEQ_2:124;
hence contradiction by A5, A6, FINSEQ_2:57; :: thesis: verum

end;

hence ( Jordan_block (L,n) is invertible iff ( n = 0 or L <> 0. K ) ) by A1; :: thesis: verum