Commit 2024-01-12 08:24 c1cd6459

View on Github →

feat: add Finset.piAntidiagonal (#7904) This is defined in terms of Finset.HasAntidiagonal. A subsequent PR #9309 uses this to compute coefficients of products of power series. Co-author : Maria Ines de Frutos Fernandez Based on work of Bhavik Mehta in Archive/Partition.lean

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/PiAntidiagonal.lean

added def Finset.finAntidiagonal

added def Finset.finAntidiagonal₀

added theorem Finset.mapRange_piAntidiagonal_eq

added theorem Finset.mapRange_piAntidiagonal_subset

added theorem Finset.mem_finAntidiagonal

added theorem Finset.mem_finAntidiagonal₀'

added theorem Finset.mem_finAntidiagonal₀

added theorem Finset.mem_piAntidiagonal'

added theorem Finset.mem_piAntidiagonal

added theorem Finset.mem_piAntidiagonal_insert

added def Finset.piAntidiagonal

added theorem Finset.piAntidiagonal_empty

added theorem Finset.piAntidiagonal_empty_of_ne_zero

added theorem Finset.piAntidiagonal_empty_of_zero

added theorem Finset.piAntidiagonal_insert

added theorem Finset.piAntidiagonal_zero

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.embDomain_comapDomain

added theorem Finsupp.prod_equivMapDomain

Modified Mathlib/Data/Finsupp/Defs.lean

Created test/antidiagonal.lean