for n being Nat
for K being Field
for M being Matrix of n,K holds
( M is lower_triangular Matrix of n,K iff M @ is upper_triangular Matrix of n,K )