Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-21 02:35 d7cea061

View on Github →

feat (ring_theory/noetherian) various lemmas (#548)

Estimated changes

Modified ring_theory/noetherian.lean

added theorem is_noetherian_of_fg_of_noetherian

added theorem is_noetherian_of_linear_equiv

added theorem is_noetherian_of_surjective

added theorem is_noetherian_pi

added theorem is_noetherian_prod

added theorem is_noetherian_ring_of_ring_equiv

added theorem is_noetherian_ring_of_surjective

added theorem is_noetherian_submodule

added theorem is_noetherian_submodule_left

added theorem is_noetherian_submodule_right

added theorem submodule.fg_bot

added theorem submodule.fg_map

added theorem submodule.fg_of_fg_map_of_fg_inf_ker

added theorem submodule.fg_prod

added theorem submodule.fg_sup