FMLJohn

feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring

2

--- [](https://gitpod.io/from-referrer/)

Feat(AlgebraicGeometry/FromSpecStalk): Given a scheme `X` and a point `x : X`, the canonical scheme morphism from `Spec(O_x)` to `X`.

4

In this pull request, we define: Given a scheme `X` and a point `x : X.carrier`, `AlgebraicGeometry.Scheme.fromSpecStalk X x` is the canonical scheme morphism from `Spec(O_x)` to `X`. This is...

Feat (RingTheory/Ideal/KrullDimension): defined the Krull dimension of a ring.

5

The ring theoretic krull dimension is the order theoretic krull dimension applied to its prime spectrum. Unfolding this definition, it is the length of longest series of prime ideals ordered...