Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-07 17:30 4421f46d

View on Github →

feat(ring_theory): submodules and quotients of Noetherian modules are Noetherian

Estimated changes

Modified algebra/order.lean

added theorem le_iff_le_of_strict_mono

Modified data/set/basic.lean

added theorem set.singleton_union

modified theorem set.union_singleton

Modified data/set/finite.lean

added theorem set.finite.exists_finset_coe

Modified linear_algebra/basic.lean

Modified linear_algebra/quotient_module.lean

added theorem quotient_module.quotient.exists_rep

Modified linear_algebra/subtype_module.lean

added theorem is_submodule.is_linear_map_inclusion

Modified order/conditionally_complete_lattice.lean

Modified order/order_iso.lean

Created ring_theory/correspondence_theorem.lean

Created ring_theory/noetherian.lean

added def is_fg

added def is_noetherian

added theorem is_noetherian_iff_well_founded

added theorem is_noetherian_of_quotient_of_noetherian

added theorem is_noetherian_of_submodule_of_noetherian

added def is_noetherian_ring

added def submodule.fg

added theorem submodule.fg_def

added def submodule.univ

Created ring_theory/submodule.lean

added theorem submodule.Union_set_of_directed

added theorem submodule.bot_set

added theorem submodule.embedding_eq

added theorem submodule.eq

added theorem submodule.ext

added theorem submodule.mem_coe

added def submodule.pullback_injective_of_surjective

added def submodule.pushforward_injective_of_injective

added theorem submodule.sInter_set

added def submodule.span

added theorem submodule.span_empty

added theorem submodule.span_subset_iff

added theorem submodule.span_union

added theorem submodule.top_set

added structure {u