for K being Ring
for A being Matrix of 0 ,K holds Det A = 1. K