From 506fd9b4d6591a7f26143f7ed2355f1e64c07a4b Mon Sep 17 00:00:00 2001 From: GTBarkley <67718465+GTBarkley@users.noreply.github.com> Date: Sat, 10 Jun 2023 18:53:44 -0400 Subject: [PATCH] added more references to mathlib to readme --- README.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 058a6e8..3c5bba6 100644 --- a/README.md +++ b/README.md @@ -18,9 +18,14 @@ class IsMaximal (I : Ideal α) : Prop - Definition of a Noetherian and Artinian rings: ```lean class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop +class Mathlib.RingTheory.Artinian.IsArtinian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop ``` +- Definition of a polynomial ring: `Mathlib.RingTheory.Polynomial.Basic` -- Definitions of a local ring and quotient ring +- Definitions of a local ring and quotient ring: `Mathlib.RingTheory.Ideal.Quotient.?` +```lean +class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] extends Nontrivial R : Prop +``` - Definition of the chain of prime ideals and the length of these chains