mathlib

186ad763 - feat(ring_theory/finiteness): add finitely presented algebra (#5407)

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.