Commit 2025-03-31 22:40 9bed6a56

View on Github →

feat(Order): more API for krull dimensions (#21800)

Estimated changes

Modified Mathlib/Algebra/Order/SuccPred/WithBot.lean

added theorem WithBot.one_le_iff_pos

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.krullDim_eq_zero

added theorem Order.krullDim_eq_zero_iff_of_orderBot

added theorem Order.krullDim_eq_zero_iff_of_orderTop

added theorem Order.krullDim_pos_iff_of_orderBot

added theorem Order.krullDim_pos_iff_of_orderTop

Modified Mathlib/Order/RelSeries.lean

added theorem Rel.finiteDimensional_swap_iff

added theorem Rel.infiniteDimensional_swap_iff

added theorem Rel.wellFounded_of_finiteDimensional

added theorem Rel.wellFounded_swap_of_finiteDimensional

added theorem RelSeries.cons_cast_succ

added theorem RelSeries.snoc_cast_castSucc