LinearMap.equivRange

Stream: Is there code for X?

[Michael Rothgang]

The analogue of docs#ContinousLinearEquiv.equivRange, but for injective linear maps --- something like this:

import Mathlib

variable {𝕜 E F : Type*} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]

example {f : E →ₗ[𝕜] F} (hf : Function.Injective f) : E ≃ₗ[𝕜] LinearMap.range f := sorry

[Aaron Liu]

docs#LinearEquiv.ofInjective

[Michael Rothgang]

Great, thank you!

[Sébastien Gouëzel]

There is also docs#ContinuousLinearMap.equivRange in the continuous category.