let n be Nat; for K being Field
for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n)
let K be Field; for M1 being Matrix of n,K holds M1 commutes_with 0. (K,n,n)
let M1 be Matrix of n,K; M1 commutes_with 0. (K,n,n)
per cases
( n > 0 or n = 0 )
by NAT_1:3;
suppose A1:
n > 0
;
M1 commutes_with 0. (K,n,n)A2:
(
len M1 = n &
width M1 = n )
by MATRIX_0:24;
then A3:
(0. (K,n,n)) * M1 = 0. (
K,
n,
n)
by Th1;
M1 * (0. (K,n,n)) = 0. (
K,
n,
n)
by A1, A2, Th2;
hence
M1 commutes_with 0. (
K,
n,
n)
by A3;
verum end; end;