Commit 2023-02-11 08:36 388222f0

View on Github →

feat: port Data.Fin.Tuple.NatAntidiagonal (#2170)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

added def Finset.Nat.antidiagonalTuple

added theorem Finset.Nat.antidiagonalTuple_one

added theorem Finset.Nat.antidiagonalTuple_two

added theorem Finset.Nat.antidiagonalTuple_zero_right

added theorem Finset.Nat.antidiagonalTuple_zero_succ

added theorem Finset.Nat.antidiagonalTuple_zero_zero

added theorem Finset.Nat.mem_antidiagonalTuple

added def Finset.Nat.sigmaAntidiagonalTupleEquivTuple

added def List.Nat.antidiagonalTuple

added theorem List.Nat.antidiagonalTuple_one

added theorem List.Nat.antidiagonalTuple_pairwise_pi_lex

added theorem List.Nat.antidiagonalTuple_two

added theorem List.Nat.antidiagonalTuple_zero_right

added theorem List.Nat.antidiagonalTuple_zero_succ

added theorem List.Nat.antidiagonalTuple_zero_zero

added theorem List.Nat.mem_antidiagonalTuple

added theorem List.Nat.nodup_antidiagonalTuple

added def Multiset.Nat.antidiagonalTuple

added theorem Multiset.Nat.antidiagonalTuple_one

added theorem Multiset.Nat.antidiagonalTuple_two

added theorem Multiset.Nat.antidiagonalTuple_zero_right

added theorem Multiset.Nat.antidiagonalTuple_zero_succ

added theorem Multiset.Nat.antidiagonalTuple_zero_zero

added theorem Multiset.Nat.mem_antidiagonalTuple

added theorem Multiset.Nat.nodup_antidiagonalTuple