mathlib3

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

refactor(*): rename `semimodule` to `module`, delete typeclasses `module` and `vector_space` (#7322) Splitting typeclasses between `semimodule`, `module` and `vector_space` was causing many (small) issues, so why don't we just get rid of this duplication? This PR contains the following changes: * delete the old `module` and `vector_space` synonyms for `semimodule` * find and replace all instances of `semimodule` and `vector_space` to `module` * (thereby renaming the previous `semimodule` typeclass to `module`) * rename `vector_space.dim` to `module.rank` (in preparation for generalizing this definition to all modules) * delete a couple `module` instances that have now become redundant This find-and-replace has been done extremely naïvely, but it seems there were almost no name clashes and no "clbuttic mistakes". I have gone through the full set of changes, finding nothing weird, and I'm fixing any build issues as they come up (I expect less than 10 declarations will cause conflicts). Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/module.20from.20semimodule.20over.20a.20ring A good example of a workaround required by the `module` abbreviation is the [`triv_sq_zero_ext.module` instance](https://github.com/leanprover-community/mathlib/blob/3b8cfdc905c663f3d99acac325c7dff1a0ce744c/src/algebra/triv_sq_zero_ext.lean#L164). Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>