[Merged by Bors] - feat(Algebra/Module): presentation of modules

[joelriou]

This PR defines a basic API for the description of modules in terms of generators and relations.

---

[github-actions]

PR summary 4c36db383d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Module.Presentation.Basic	892

---

Declarations diff

+ IsPresentation
+ Presentation
+ Quotient
+ Relations
+ Solution
+ desc
+ desc_var
+ exact
+ fromQuotient
+ fromQuotient_comp_toQuotient
+ fromQuotient_mk
+ ker_toQuotient
+ ker_π
+ linearEquiv
+ linearEquiv_apply
+ linearEquiv_symm_var
+ linearMapEquiv
+ map
+ mapToKer
+ mapToKer_coe
+ map_single
+ ofQuotient
+ ofQuotient_fromQuotient
+ ofQuotient_isPresentation
+ ofQuotient_π
+ ofπ
+ ofπ'
+ ofπ'_π
+ ofπ_π
+ postcomp
+ postcomp_injective
+ range_map
+ span_relation_le_ker_π
+ surjective_mapToKer
+ surjective_toQuotient
+ surjective_π
+ toQuotient
+ toQuotient_relation
+ π
+ π_comp_map
+ π_comp_map_apply
+ π_relation
+ π_single

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[erdOne]

Looks nice!
Some feature request & design choice questions.

[joelriou]

Thanks very much @erdOne for the review!

[erdOne]

LGTM
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

Thanks! Left 1 comment

bors d+

[mathlib-bors]

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

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style