Commit 2023-03-20 19:32 f411c38b

View on Github →

feat: port RingTheory.Noetherian (#2976)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Noetherian.lean

added theorem IsNoetherian.bijective_of_surjective_endomorphism

added theorem IsNoetherian.disjoint_partialSups_eventually_bot

added theorem IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot

added theorem IsNoetherian.induction

added theorem IsNoetherian.injective_of_surjective_endomorphism

added theorem IsNoetherianRing.isNilpotent_nilradical

added def IsNoetherianRing

added theorem Module.Finite.of_injective

added theorem fg_of_injective

added theorem fg_of_ker_bot

added theorem finite_of_linearIndependent

added theorem isNoetherianRing_iff

added theorem isNoetherianRing_iff_ideal_fg

added theorem isNoetherianRing_of_ringEquiv

added theorem isNoetherianRing_of_surjective

added theorem isNoetherian_def

added theorem isNoetherian_iff_fg_wellFounded

added theorem isNoetherian_iff_wellFounded

added theorem isNoetherian_of_fg_of_noetherian'

added theorem isNoetherian_of_fg_of_noetherian

added theorem isNoetherian_of_injective

added theorem isNoetherian_of_ker_bot

added theorem isNoetherian_of_le

added theorem isNoetherian_of_linearEquiv

added theorem isNoetherian_of_range_eq_ker

added theorem isNoetherian_of_submodule_of_noetherian

added theorem isNoetherian_of_surjective

added theorem isNoetherian_of_tower

added theorem isNoetherian_span_of_finite

added theorem isNoetherian_submodule

added theorem isNoetherian_submodule_left

added theorem isNoetherian_submodule_right

added theorem isNoetherian_top_iff

added theorem monotone_stabilizes_iff_noetherian

added theorem set_has_maximal_iff_noetherian

added theorem wellFounded_submodule_gt