mathlib3

3397560e - chore(topology/algebra/module/basic): remove `continuous_linear_map.ker` and `continuous_linear_map.range` (#16208)

chore(topology/algebra/module/basic): remove `continuous_linear_map.ker` and `continuous_linear_map.range` (#16208) This PR removes `continuous_linear_map.ker` and `continuous_linear_map.range`, which are now obsolete since `linear_map.ker` and `linear_map.range` are defined for any `linear_map_class` morphism.