Commit 2022-02-15 17:47 52aaf173

View on Github →

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.

Estimated changes

Modified src/data/finset/nat_antidiagonal.lean

added theorem finset.nat.antidiagonal_succ'

added theorem finset.nat.antidiagonal_succ_succ'

Modified src/data/list/nat_antidiagonal.lean

added theorem list.nat.antidiagonal_succ'

added theorem list.nat.antidiagonal_succ_succ'

added theorem list.nat.map_swap_antidiagonal

Modified src/data/multiset/nat_antidiagonal.lean

added theorem multiset.nat.antidiagonal_succ'

added theorem multiset.nat.antidiagonal_succ_succ'

added theorem multiset.nat.map_swap_antidiagonal