Commit 2020-05-30 16:24 67f1951b

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_monoids. 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.