Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-06 11:04 186ad763

View on Github →

feat(ring_theory/finiteness): add finitely presented algebra (#5407) This PR contains the definition of a finitely presented algebra and some very basic results. A lot of other fundamental results are missing (stability under composition, equivalence with finite type for noetherian rings ecc): I am ready to work on them, but I wanted some feedback. Feel free to convert to WIP if you think it's better to wait.

Estimated changes