Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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>
- Loading branch information