Commit 2021-12-23 19:11 cce09a6b

feat(ring_theory/finiteness): prove that a surjective endomorphism of a finite module over a comm ring is injective (#10944) Using an approach of Vasconcelos, treating the module as a module over the polynomial ring, with action induced by the endomorphism. This result was rescued from #1822.