Def RelSeries.fromListChain'

Modification history

2025-09-24 16:53

Mathlib/Order/RelSeries.lean

fix: adaptations for batteries#1421 (#29928) …

Deleted RelSeries.fromListChain'View on Github →

2025-07-06 13:16

Mathlib/Order/RelSeries.lean

refactor: make `Rel` less see-through (#25587) …

Modified RelSeries.fromListChain'View on Github →

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 →