Commit 2022-06-29 02:12 55ec65a6

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.