Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-10 11:25 d3fff8a0

View on Github →

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

Estimated changes

added theorem fin.cons_le
added theorem fin.eq_insert_nth_iff
added def fin.insert_nth
added theorem fin.insert_nth_eq_iff
added theorem fin.insert_nth_last'
added theorem fin.insert_nth_last
added theorem fin.insert_nth_zero'
added theorem fin.insert_nth_zero
added theorem fin.le_cons
added theorem fin.pred_above_zero
deleted theorem fin.succ_above_descend
modified theorem fin.succ_above_lt_iff
added theorem fin.tuple0_le