∀ (R : Type u_1) (n : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ AlgHom.mulLeftRightMatrix_inv R n = LinearMap.id