mathlib3

34020e53 - chore(linear_algebra/basic): generalize `submodule.map`, `comap`, etc to `semilinear_map_class` (#16105)

chore(linear_algebra/basic): generalize `submodule.map`, `comap`, etc to `semilinear_map_class` (#16105) This PR generalizes `submodule.map`, `submodule.comap`, `linear_map.ker` and `linear_map.range` such that they are defined for any morphism class satisfying `semilinear_map_class` (they are currently hardcoded for `linear_map`s). The namespaces have been left as is. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>