:: deftheorem Def3 defines Rotation MATRTOP3:def 3 :
for n being Nat
for r being Real
for i, j being Nat st 1 <= i & i < j & j <= n holds
for b₅ being invertible Matrix of n,F_Real holds
( b₅ = Rotation (i,j,n,r) iff ( b₅ * (i,i) = cos r & b₅ * (j,j) = cos r & b₅ * (i,j) = sin r & b₅ * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b₅ holds
( ( k = m & k <> i & k <> j implies b₅ * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b₅ * (k,m) = 0. F_Real ) ) ) ) );