Commit 2024-01-17 20:26 c8766486

View on Github →

feat: injective continuous linear map with closed range is a continuous linear equivalence (#9756) Added analogue of LinearEquiv.ofInjective but for ContinuousLinearEquiv on Banach spaces. Added analogue of LinearMap.rangeRestrict but for ContinuousLinearMap. Also I updated a docstring that had the old name of a theorem.

Estimated changes