Commit 2024-09-28 16:22 3fdf4775

View on Github →

feat(RingTheory/Ideal/KrullDimension): define the Krull dimension of a ring (#14134) 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 by inclusion.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.LTSeries.length_le_krullDim

added theorem Order.krullDim_nonpos_of_subsingleton

Created Mathlib/RingTheory/KrullDimension/Basic.lean

added theorem ringKrullDim_eq_bot_of_subsingleton

added theorem ringKrullDim_eq_of_ringEquiv

added theorem ringKrullDim_le_of_surjective

added theorem ringKrullDim_nonneg_of_nontrivial

added theorem ringKrullDim_quotient_le

Created Mathlib/RingTheory/KrullDimension/Field.lean

added theorem ringKrullDim_eq_zero_of_field

added theorem ringKrullDim_eq_zero_of_isField

Modified Mathlib/Topology/KrullDimension.lean

Modified scripts/noshake.json