mathlib

55ec65a6 - feat(topology/algebra/module/basic): define continuous_(semi)linear_map_class (#14674)

feat(topology/algebra/module/basic): define continuous_(semi)linear_map_class (#14674) This PR brings the morphism refactor to continuous (semi)linear maps. We define `continuous_semilinear_map_class` and `continuous_linear_map_class` in a way that parallels the non-continuous versions, along with a few extras (i.e. `add_monoid_hom_class` instance for `normed_group_hom`). A few things I was not too sure about: - When generalizing lemmas to a morphism class rather than a particular type of morphism, I used `𝓕` as the type (instead of just `F` as is done for most `fun_like` types) to avoid clashing with our convention of using `E`, `F`, etc for e.g. vector spaces. - Namespacing: I placed lemmas like `isometry_of_norm`, `continuous_of_bound`, etc, under the `add_monoid_hom_class` namespace. Maybe the root namespace would make sense here. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>