mathlib

240836ae - feat(analysis/normed_space/basic): generalize submodule.normed_space (#6766)

feat(analysis/normed_space/basic): generalize submodule.normed_space (#6766) This means that a ℂ-submodule of an ℝ-normed space is still an ℝ-normed space. There's too much randomness in the profiling for me to tell if this speeds up or slows down `exists_extension_norm_eq`; but it does at least save a line there.