theorem :: MATGRP_0:153

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