Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 15:00 3b09a260

View on Github →

feat(ring_theory/artinian): localization maps of artinian rings are surjective (#15736) The proof is by Junyan, I just tidied it up a little, and also the ring_theory/artinian file a little bit, in order to fit the results more smoothly.

Estimated changes

Modified src/ring_theory/artinian.lean

added theorem function.surjective.is_artinian_ring

modified theorem is_artinian.bijective_of_injective_endomorphism

modified theorem is_artinian.disjoint_partial_infs_eventually_top

modified theorem is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top

added theorem is_artinian.exists_pow_succ_smul_dvd

modified theorem is_artinian.induction

modified theorem is_artinian.monotone_stabilizes

added theorem is_artinian.range_smul_pow_stabilizes

modified theorem is_artinian.surjective_of_injective_endomorphism

deleted theorem is_artinian_of_fintype

added theorem is_artinian_ring.localization_artinian

added theorem is_artinian_ring.localization_surjective

deleted theorem is_artinian_ring_of_ring_equiv

deleted theorem is_artinian_ring_of_surjective

Modified src/ring_theory/localization/cardinality.lean

deleted theorem is_localization.algebra_map_surjective_of_fintype