Commit 2024-12-29 20:14 b4e1f959

View on Github →

feat(Order/KrullDimension): equivalent conditions for zero-dimensional, one-dimensional etc (#20176)

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem WithBot.add_one_le_iff

added theorem WithBot.lt_add_one_iff

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.krullDim_eq_bot

added theorem Order.krullDim_eq_bot_iff

deleted theorem Order.krullDim_eq_bot_of_isEmpty

added theorem Order.krullDim_eq_top

added theorem Order.krullDim_eq_top_iff

deleted theorem Order.krullDim_eq_top_of_infiniteDimensionalOrder

modified theorem Order.krullDim_eq_zero_of_unique

added theorem Order.krullDim_le_one_iff

added theorem Order.krullDim_le_one_iff_forall_isMax

added theorem Order.krullDim_le_one_iff_forall_isMin

added theorem Order.krullDim_lt_coe_iff

added theorem Order.krullDim_nonneg

added theorem Order.krullDim_nonneg_iff

deleted theorem Order.krullDim_nonneg_of_nonempty

added theorem Order.krullDim_nonpos_iff_forall_isMax

added theorem Order.krullDim_nonpos_iff_forall_isMin

added theorem Order.krullDim_pos_iff

added theorem Order.le_krullDim_iff

added theorem Order.one_le_krullDim_iff

Modified Mathlib/Order/RelSeries.lean

added theorem Rel.finiteDimensional_or_infiniteDimensional

added theorem Rel.not_finiteDimensional_iff

added theorem Rel.not_infiniteDimensional_iff

added theorem finiteDimensionalOrder_or_infiniteDimensionalOrder

added theorem not_finiteDimensionalOrder_iff

added theorem not_infiniteDimensionalOrder_iff

Modified Mathlib/RingTheory/KrullDimension/Basic.lean