Theorem complex.{u}

refactor(linear_algebra/dimension): use `rank` in lemma names instead of `dim` (#18741) …

refactor(set_theory/{cardinal,ordinal}): swap the order of universes in `lift` (#9273) …

refactor(*): rename `semimodule` to `module`, delete typeclasses `module` and `vector_space` (#7322) …

feat(data/complex/module): ![1, I] is a basis of C over R (#4713)