Commit 2020-08-26 14:45 0d67a02d

feat(ring_theory/noetherian): maximal among set iff Noetherian (#3846) Main theorem is set_has_maximal_iff_noetherian, which relates well foundedness of < to being noetherian. Most notably a result of well_founded.well_founded_iff_has_max' provides the fact that on a partial ordering, well_founded > is equivalent to each nonempty set having a maximal element. well_founded.well_founded_iff_has_min provides an analogous fact for well_founded <. Some other miscellaneous lemmas are as follows localization_map.integral_domain_of_local_at_prime is the localization of an integral domain at a prime's complement is an integral domain ideal.mul_eq_bot is the fact that in an integral domain if I*J = 0, then at least one is 0. submodule.nonzero_mem_of_gt_bot is that if ⊥ < J, then J has a nonzero member. lt_add_iff_not_mem is that b is not a member of J iff J < J+(b). bot_prime states that 0 is a prime ideal of an integral domain.