mathlib3
8454c108 - doc(ring_theory/noetherian): add docstring, normalise notation (#2219)

Commit
5 years ago
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 Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading