theorem Th172: :: MATGRP_0:152

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds inverse_op G = (inverse_op (GL (n,R))) | the carrier of G