LinearMap.range for ContinuousLinearMap

Stream: mathlib4

[Yury G. Kudryashov]

While working on https://github.com/urkud/SardMoreira, I had to workaround the fact that docs#LinearMap.range is define for a typeclass, but lacks API for anything but LinearMaps. @Yaël Dillies AFAIR, you had plans to fix this one way or another. Am I right? If yes, then what's the plan?

[Yaël Dillies]

I am currently working on two big refactors: monoid algebras in #25273 and torsion-free modules in #30563. Once one of these refactors is completed, I will resume work on the refactor you mention

[Yaël Dillies]

Note that @Jireh Loreaux has given a concrete plan in another thread (although I disagree with the details of the plan)

[Junyan Xu]

There's #25138 to restrict RingHom.ker to RingHom, and I suppose we're going to do the same thing for LinearMap.ker/range.