Def CompositionSeries.ofList

Modification history

2024-05-30 11:03

Mathlib/Order/JordanHolder.lean

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

Deleted CompositionSeries.ofList View on Github →

2024-05-17 19:31

Mathlib/Order/JordanHolder.lean

style: remove all isolated `where` (#12991)

Modified CompositionSeries.ofList View on Github →

2023-03-08 14:42

Mathlib/Order/JordanHolder.lean

feat: port Order.JordanHolder (#2578)

Added CompositionSeries.ofList View on Github →