Theorem WithBot.lt_add_one_iff

Modification history

2024-12-29 20:14

Mathlib/Data/ENat/Basic.lean

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

Added WithBot.lt_add_one_iff View on Github →