Commit 2023-09-18 04:21 dd840899
View on Github →feat: rework StrictSeries
to RelSeries
(#7221)
I amend the definition of StrictSeries
according to this thread
Now a RelSeries r
of length n
is $a_0 \stackrel{r}{\to} a_1 \stackrel{r}{\to} \dots \stackrel{r}{\to} a_n$.
In case r
is transitive, then p : RelSeries r
implies that the underlying function of r
is strictly monotonic.
Then if $\alpha$ is a preordered set, an LTSeries
is a RelSeries (. < .)
and its Krull dimension is defined as the supremum of length of LTSeries
.
For future: now CompositionSeries
is RelSeries jordan_holder_lattice.is_maximal
and rework the Jordan Holder file