Commit 2024-06-27 01:16 c95b27fc

View on Github →

feat(Order/KrullDimension): add some basic lemmas about krull dimension of a preorder (#11147)

krull dimension, height, coheight interacting with functions
order dual These will be specialized to ring theoretic krull dimension later

Estimated changes

Modified Mathlib/Order/KrullDimension.lean

added theorem height_mono

added theorem krullDim_eq_bot_of_isEmpty

added theorem krullDim_eq_iSup_height

added theorem krullDim_eq_length_of_finiteDimensionalOrder

added theorem krullDim_eq_of_orderIso

added theorem krullDim_eq_top_of_infiniteDimensionalOrder

added theorem krullDim_eq_zero_of_unique

added theorem krullDim_le_of_strictComono_and_surj

added theorem krullDim_le_of_strictMono

added theorem krullDim_nonneg_of_nonempty

added theorem krullDim_orderDual

Modified Mathlib/Order/RelSeries.lean

added theorem infiniteDimensionalOrder_of_strictMono