theorem :: MATRIX11:53

for n being Nat
for K being commutative Ring
for a being Element of K
for A being Matrix of n,K
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det A = Det (RLine (A,i,((Line (A,i)) + (a * (Line (A,j))))))