nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339)

Commit

3 years ago

feat(data/fin/tuple/nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339) This proof feels a little clumsy, but maybe that's unavoidable.

Author

eric-wieser

Parents

9380977b

mathlib b90e770f - feat(data/fin/tuple/nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339)

mathlib
b90e770f - feat(data/fin/tuple/nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339)