:: deftheorem Def12 defines matrix_inv MATGRP_0:def 12 :
for n being Nat
for R being Ring
for b₃ being UnOp of (n -invertible_Matrices_over R) holds
( b₃ = matrix_inv (n,R) iff for x being Element of n -invertible_Matrices_over R
for X being invertible Matrix of n,R st x = X holds
b₃ . x = X ~ );