mathlib3
2f5533c9 - feat(ring_theory/finiteness): Kernel of surjective morphism between finitely presented algebras is fg. (#15969)
