Commit 2023-09-18 04:21 dd840899

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