nat_antidiagonal): add lemmas to remove elements from head and tail of antidiagonal (#12028)

Commit

3 years ago

feat(data/{list,multiset,finset}/nat_antidiagonal): add lemmas to remove elements from head and tail of antidiagonal (#12028) Also lowered `finset.nat.map_swap_antidiagonal` down to `list` through `multiset`.

Author

kmill

Parents

c0c673ab

mathlib3 52aaf173 - feat(data/{list,multiset,finset}/nat_antidiagonal): add lemmas to remove elements from head and tail of antidiagonal (#12028)

mathlib3
52aaf173 - feat(data/{list,multiset,finset}/nat_antidiagonal): add lemmas to remove elements from head and tail of antidiagonal (#12028)