Commit 2023-02-07 13:59 b00ce534

View on Github →

feat: port Data.Finsupp.Antidiagonal (#2142)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Antidiagonal.lean

added def Finsupp.antidiagonal'

added def Finsupp.antidiagonal

added theorem Finsupp.antidiagonal_filter_fst_eq

added theorem Finsupp.antidiagonal_filter_snd_eq

added theorem Finsupp.antidiagonal_zero

added theorem Finsupp.mem_antidiagonal

added theorem Finsupp.prod_antidiagonal_swap

added theorem Finsupp.swap_mem_antidiagonal