:: deftheorem defines -invertible_Matrices_over MATGRP_0:def 11 :
for n being Nat
for R being Ring holds n -invertible_Matrices_over R = { X where X is Element of n -Matrices_over R : X is invertible Matrix of n,R } ;