Commit 2023-05-08 09:17 b81e3639

feat: definition of krull dimension for a preordered set (#3704) Given a preordered set $(S, <)$, the krull dimension of $S$ is defined to be $\sup{n | a_0 < a_1 < ... < a_n}$ where the supremum takes place in extended natural numbers $\mathbb N \cup {\pm \infty}$, i.e. empty set is negative-infinite dimensional and a set with arbitrary long $a_0 < a_1 < ... < a_n$ is positive dimensional. Similar constructions in mathlib does require a chain to be nonempty so that empty set would have the wrong dimension, so I defined a new structure StrictSeries to avoid confusion with chain; in this structure, the underlying list is always nonempty.