:: deftheorem defines GL MATGRP_0:def 10 :
for n being Nat
for R being Ring holds GL (n,R) = UnitGroup (Matrix_ring (n,R));