mathlib3

cce09a6b - feat(ring_theory/finiteness): prove that a surjective endomorphism of a finite module over a comm ring is injective (#10944)

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.