Def CompositionSeries.append

Modification history

2024-05-30 11:03

Mathlib/Order/JordanHolder.lean

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

Deleted CompositionSeries.append View on Github →

2023-03-08 14:42

Mathlib/Order/JordanHolder.lean

feat: port Order.JordanHolder (#2578)

Added CompositionSeries.append View on Github →