let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st M1 is Nilpotent & n > 0 holds
M1 @ is Nilpotent
let K be Field; :: thesis: for M1 being Matrix of n,K st M1 is Nilpotent & n > 0 holds
M1 @ is Nilpotent
let M1 be Matrix of n,K; :: thesis: ( M1 is Nilpotent & n > 0 implies M1 @ is Nilpotent )
assume that
A1: M1 is Nilpotent and
A2: n > 0 ; :: thesis: M1 @ is Nilpotent
( len M1 = n & width M1 = n ) by MATRIX_0:24;
then (M1 @) * (M1 @) = (M1 * M1) @ by A2, MATRIX_3:22
.= (0. (K,n)) @ by A1
.= (n,n) --> (0. K) by MATRIX_6:20
.= 0. (K,n) ;
hence M1 @ is Nilpotent ; :: thesis: verum