mathlib3

3959a8bb - perf(ring_theory/{noetherian,ideal/basic}): Simplify proofs of Krull's theorem and related theorems (#6082)

perf(ring_theory/{noetherian,ideal/basic}): Simplify proofs of Krull's theorem and related theorems (#6082) Move `submodule.singleton_span_is_compact_element` and `submodule.is_compactly_generated` to more appropriate locations. Add trivial order isomorphisms and order-iso lemmas. Show that `is_atomic` and `is_coatomic` are respected by order isomorphisms. Greatly simplify `is_noetherian_iff_well_founded`. Provide an `is_coatomic` instance on the ideal lattice of a ring and simplify `ideal.exists_le_maximal`.