Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-29 02:52 8454c108

View on Github →

doc(ring_theory/noetherian): add docstring, normalise notation (#2219)

change notation; add module docstring
adding reference to A-M
Update src/ring_theory/noetherian.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
Apply suggestions from code review

Estimated changes

Modified docs/references.bib

Modified src/ring_theory/noetherian.lean

modified theorem finite_of_linear_independent

modified theorem is_noetherian_of_fg_of_noetherian

modified theorem is_noetherian_of_linear_equiv

modified theorem is_noetherian_of_quotient_of_noetherian

modified theorem is_noetherian_of_submodule_of_noetherian

modified theorem is_noetherian_of_surjective

modified theorem is_noetherian_ring.exists_factors

modified theorem is_noetherian_ring.exists_irreducible_factor

modified theorem is_noetherian_ring.irreducible_induction_on

modified theorem is_noetherian_ring.well_founded_dvd_not_unit

modified def is_noetherian_ring

modified theorem is_noetherian_span_of_finite

modified theorem is_noetherian_submodule

modified theorem is_noetherian_submodule_left

modified theorem is_noetherian_submodule_right

modified def submodule.fg

modified theorem submodule.fg_bot

modified theorem submodule.fg_def

modified theorem submodule.fg_map

modified theorem submodule.fg_of_fg_map_of_fg_inf_ker

modified theorem submodule.fg_pow

modified theorem submodule.fg_prod

modified theorem submodule.fg_sup

modified theorem well_founded_submodule_gt