Commit 2023-05-21 22:16 870712fc

View on Github →

feat: port RingTheory.Artinian (#4104)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Artinian.lean

added theorem Function.Surjective.isArtinianRing

added theorem IsArtinian.bijective_of_injective_endomorphism

added theorem IsArtinian.disjoint_partial_infs_eventually_top

added theorem IsArtinian.exists_endomorphism_iterate_ker_sup_range_eq_top

added theorem IsArtinian.exists_pow_succ_smul_dvd

added theorem IsArtinian.finite_of_linearIndependent

added theorem IsArtinian.induction

added theorem IsArtinian.monotone_stabilizes

added theorem IsArtinian.range_smul_pow_stabilizes

added theorem IsArtinian.set_has_minimal

added theorem IsArtinian.surjective_of_injective_endomorphism

added theorem IsArtinian.wellFounded_submodule_lt

added theorem IsArtinianRing.isNilpotent_jacobson_bot

added theorem IsArtinianRing.localization_artinian

added theorem IsArtinianRing.localization_surjective

added def IsArtinianRing

added theorem Ring.isArtinian_of_zero_eq_one

added theorem isArtinianRing_iff

added theorem isArtinian_iff_wellFounded

added theorem isArtinian_of_fg_of_artinian'

added theorem isArtinian_of_fg_of_artinian

added theorem isArtinian_of_injective

added theorem isArtinian_of_le

added theorem isArtinian_of_linearEquiv

added theorem isArtinian_of_quotient_of_artinian

added theorem isArtinian_of_range_eq_ker

added theorem isArtinian_of_submodule_of_artinian

added theorem isArtinian_of_surjective

added theorem isArtinian_of_tower

added theorem isArtinian_span_of_finite

added theorem monotone_stabilizes_iff_artinian

added theorem set_has_minimal_iff_artinian