mathlib3

0d67a02d - feat(ring_theory/noetherian): maximal among set iff Noetherian (#3846)

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. Co-authored-by: mushokunosora <knaka3435@gmail.com> Co-authored-by: mushokunosora <38799099+mushokunosora@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>