# Commit 2020-05-30 16:24 67f1951b

View on Github →refactor(algebra/module): change module into an abbreviation for semimodule (#2848)
The file `algebra/module.lean`

contains the lines

```
There were several attempts to make `module` an abbreviation of `semimodule` but this makes
class instance search too hard for Lean 3.
```

It turns out that this was too hard for Lean 3 until recently, but this is not too hard for Lean 3.14. This PR removes these two lines, and changes the files accordingly.
This means that the basic objects of linear algebra are now semimodules over semiring, making it possible to talk about matrices with natural number coefficients or apply general results on multilinear maps to get the binomial or the multinomial formula.
A linear map is now defined over semirings, between semimodules which are `add_comm_monoid`

s. For some statements, you need to have an `add_comm_group`

, and a `ring`

or a `comm_semiring`

or a `comm_ring`

. I have not tried to lower the possible typeclass assumptions like this in all files, but I have done it carefully in the following files:

`algebra/module`

`linear_algebra/basic`

`linear_algebra/multilinear`

`topology/algebra/module`

`topology/algebra/multilinear`

Other files can be optimised later in the same way when needed, but this PR is already big enough. I have also fixed the breakage in all the other files. It was sometimes completely mysterious (in tensor products, I had to replace several times`linear_map.id.flip`

with`linear_map.flip linear_map.id`

), but globally all right. I have tweaked a few instance priorities to make sure that things don't go too bad: there are often additional steps in typeclass inference, going from`ring`

to`semiring`

and from`add_comm_group`

to`add_comm_monoid`

, so I have increased their priority (putting it strictly between 100 and 1000), and adjusted some other priorities to get more canonical instance paths, fixing some preexisting weirdnesses (notably in multilinear maps). One place where I really had to help Lean is with normed spaces of continuous multilinear maps, where instance search is just too big. I am aware that this will be a nightmare to refer, but as often with big refactor it's an "all or nothing" PR, impossible to split in tiny pieces.