Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-10 19:34 0bc2aa91

View on Github →

feat(data/fin/tuple/nat_antidiagonal): add antidiagonal_tuple (#13031)

Estimated changes

Created src/data/fin/tuple/nat_antidiagonal.lean

added def finset.nat.antidiagonal_tuple

added theorem finset.nat.antidiagonal_tuple_one

added theorem finset.nat.antidiagonal_tuple_two

added theorem finset.nat.antidiagonal_tuple_zero_succ

added theorem finset.nat.antidiagonal_tuple_zero_zero

added theorem finset.nat.mem_antidiagonal_tuple

added def list.nat.antidiagonal_tuple

added theorem list.nat.antidiagonal_tuple_one

added theorem list.nat.antidiagonal_tuple_two

added theorem list.nat.antidiagonal_tuple_zero_succ

added theorem list.nat.antidiagonal_tuple_zero_zero

added theorem list.nat.mem_antidiagonal_tuple

added theorem list.nat.nodup_antidiagonal_tuple

added def multiset.nat.antidiagonal_tuple

added theorem multiset.nat.antidiagonal_tuple_one

added theorem multiset.nat.antidiagonal_tuple_two

added theorem multiset.nat.antidiagonal_tuple_zero_succ

added theorem multiset.nat.antidiagonal_tuple_zero_zero

added theorem multiset.nat.mem_antidiagonal_tuple

added theorem multiset.nat.nodup_antidiagonal_tuple