Commit 2021-02-16 12:05 314f5ad7
View on Github →feat(ring_theory/finiteness): add quotient of finitely presented (#6098)
I've added algebra.finitely_presented.quotient: the quotient of a finitely presented algebra by a finitely generated ideal is finitely presented. To do so I had to prove some preliminary results about finitely generated modules.