Commit 2021-02-11 06:02 3959a8bb
View on Github →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.