Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-20 08:06 c5951f32

View on Github →

feat(ring_theory/noetherian): a surjective endomorphism of a noetherian module is injective (#7676)

Estimated changes

Modified src/linear_algebra/basic.lean

added def linear_map.iterate_ker

added def linear_map.iterate_range

Modified src/ring_theory/noetherian.lean

added theorem is_noetherian.bijective_of_surjective_endomorphism

added theorem is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot

added theorem is_noetherian.injective_of_surjective_endomorphism

added theorem monotone_stabilizes_iff_noetherian