equivMapOfInjective for linear maps

Stream: Is there code for X?

[Alena Gusakov]

So there is a def equivMapOfInjective that takes an injective map & submodule and turns it into a semilinear equivalence between the submodule and its image Submodule.map. Is there a def somewhere that takes an injective linear map and turns it into a linear equivalence? If not, is there a mathematical reason why that wouldn't work?