mathlib3

30449be1 - feat(data/complex/is_R_or_C): generalize `is_R_or_C.proper_space_span_singleton` to all finite dimensional submodules (#12877)

feat(data/complex/is_R_or_C): generalize `is_R_or_C.proper_space_span_singleton` to all finite dimensional submodules (#12877) Also goes on to show that finite supremums of finite_dimensional submodules are finite-dimensional.