Def RelSeries.fromListChain'

Modification history

2024-05-30 11:03

Mathlib/Order/RelSeries.lean

refactor(Order/JordanHolder): use `RelSeries` to implement `CompositionSeries` (#12914) …

Modified RelSeries.fromListChain'View on Github →

2023-09-18 04:21

Mathlib/Order/RelSeries.lean

feat: rework `StrictSeries` to `RelSeries` (#7221) …

Added RelSeries.fromListChain'View on Github →