Def RelSeries.drop

Modification history

2024-08-07 14:17
Mathlib/Order/RelSeries.lean
feat(RelSeries): RelSeries.take and RelSeries.drop (#15557) …
Added RelSeries.dropView on Github →