Commit 2023-01-17 11:37 76df73b5

View on Github →

feat port : Data.Finset.NatAntidiagonal (#1598)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/NatAntidiagonal.lean

added theorem Finset.Nat.antidiagonal.fst_le

added theorem Finset.Nat.antidiagonal.snd_le

added def Finset.Nat.antidiagonal

added theorem Finset.Nat.antidiagonal_congr

added theorem Finset.Nat.antidiagonal_succ'

added theorem Finset.Nat.antidiagonal_succ

added theorem Finset.Nat.antidiagonal_succ_succ'

added theorem Finset.Nat.antidiagonal_zero

added theorem Finset.Nat.card_antidiagonal

added theorem Finset.Nat.filter_fst_eq_antidiagonal

added theorem Finset.Nat.filter_snd_eq_antidiagonal

added theorem Finset.Nat.map_swap_antidiagonal

added theorem Finset.Nat.mem_antidiagonal

added def Finset.Nat.sigmaAntidiagonalEquivProd