Commit 2024-07-05 08:34 a8fb8074

View on Github →

feat: Antidiagonal as a Finset (ι → μ) (#13683)

Estimated changes

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified Mathlib/Algebra/Order/Antidiag/Finsupp.lean

deleted def Finset.finAntidiagonal₀

modified theorem Finset.finsuppAntidiag_empty

modified theorem Finset.finsuppAntidiag_empty_of_ne_zero

modified theorem Finset.finsuppAntidiag_empty_zero

modified theorem Finset.finsuppAntidiag_insert

modified theorem Finset.finsuppAntidiag_zero

deleted theorem Finset.mem_finAntidiagonal₀'

deleted theorem Finset.mem_finAntidiagonal₀

modified theorem Finset.mem_finsuppAntidiag'

modified theorem Finset.mem_finsuppAntidiag

modified theorem Finset.mem_finsuppAntidiag_insert

Modified Mathlib/Algebra/Order/Antidiag/Pi.lean

added theorem Finset.finsetCongr_piAntidiag_eq_antidiag

added theorem Finset.map_nsmul_piAntidiag

added theorem Finset.map_nsmul_piAntidiag_univ

added theorem Finset.mem_piAntidiag

added theorem Finset.nsmul_piAntidiag

added theorem Finset.nsmul_piAntidiag_univ

added theorem Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbedding

added def Finset.piAntidiag

added theorem Finset.piAntidiag_cons

added theorem Finset.piAntidiag_empty

added theorem Finset.piAntidiag_empty_of_ne_zero

added theorem Finset.piAntidiag_empty_zero

added theorem Finset.piAntidiag_insert

added theorem Finset.piAntidiag_univ_fin_eq_antidiagonalTuple

added theorem Finset.piAntidiag_zero

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.coe_onFinset