Def CompositionSeries.eraseTop

Modification history

2024-05-30 11:03

Mathlib/Order/JordanHolder.lean

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

Deleted CompositionSeries.eraseTop View on Github →

2023-07-13 01:24

Mathlib/Order/JordanHolder.lean

chore: bump to nightly-2023-07-01 (#5409) …

Modified CompositionSeries.eraseTop View on Github →

2023-03-08 14:42

Mathlib/Order/JordanHolder.lean

feat: port Order.JordanHolder (#2578)

Added CompositionSeries.eraseTop View on Github →