mathlib
ed231516 - feat(data/list/rdrop): drop or take from the right (#15475)

Commit

3 years ago

feat(data/list/rdrop): drop or take from the right (#15475)

Author

pechersky

pechersky

Parents

Loading