Commit 2022-07-28 02:26 cad19073

chore(topology/algebra/module, analysis/normed_space/linear_isometry): dedup submodule.subtypeL and continuous_linear_map.subtype_val (#15700) To designate the continuous linear inclusion of a submodule into the ambient space, we currently have both continuous_linear_map.subtype_val (correct assumptions, name not consistent with submodule.subtype) and submodule.subtypeL (good name, but way too strong assumptions). This keeps the best of both worlds.