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.