theorem :: MATGRP_0:145

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds the carrier of G c= n -invertible_Matrices_over R