:: deftheorem defines -G_Matrix_over MATRIX_1:def 7 :
for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for n being Nat
for b₃ being strict AbGroup holds
( b₃ = n -G_Matrix_over F iff ( the carrier of b₃ = n -Matrices_over F & ( for A, B being Matrix of n,F holds the addF of b₃ . (A,B) = A + B ) & 0. b₃ = 0. (F,n) ) );