[Merged by Bors] - feat(algebra/module/torsion): define torsion submodules

[pbazin]

This file defines the a-torsion and torsion submodules for a R-module M and gives some basic properties. (The ultimate goal I'm working on is to classify the finitely-generated modules over a PID).

---

[riccardobrasca]

Thanks!

bors d+

[bors]

✌️ pbazin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[pbazin]

bors r+

[pbazin]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed:

• Build mathlib

[riccardobrasca]

You probably need to merge master and see what has changed.

[pbazin]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[fpvandoorn]

bors r-
bors d+

it seems that this PR causes an error

[bors]

✌️ pbazin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors]

Canceled.

[riccardobrasca]

There is the following error

/home/lean/actions-runner/_work/mathlib/mathlib/src/algebra/module/torsion.lean:138:28: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    function.surjective.module_left ?m_9 ideal.quotient.mk_surjective
  term
    ideal.quotient.mk_surjective
  has type
    function.surjective ⇑(ideal.quotient.mk ?m_3)
  but is expected to have type
    function.surjective ⇑?m_5

Please fix it before merging the PR. Thanks!

[pbazin]

I couldn't reproduce the error locally and merging master didn't work but now it's fixed... but I still have no idea why it wasn't able to infer the implicit arguments

[pbazin]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests