mathlib
d3fff8a0 - feat(data/fin): define `fin.insert_nth` (#4947)

Commit

5 years ago

feat(data/fin): define `fin.insert_nth` (#4947) Also rename `fin.succ_above_descend` to `fin.succ_above_pred_above`.

Author

urkud

Parents