Theorem CompositionSeries.toList_sorted

Modification history

2025-12-05 15:16
Mathlib/Order/JordanHolder.lean
refactor(`Data/List/Sort`): deprecate and replace `List.Sorted` (#30441) …
Modified CompositionSeries.toList_sortedView on Github →
2023-03-08 14:42
Mathlib/Order/JordanHolder.lean
feat: port Order.JordanHolder (#2578)
Added CompositionSeries.toList_sortedView on Github →