mathlib3

314f5ad7 - feat(ring_theory/finiteness): add quotient of finitely presented (#6098)

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.