Commit 2024-06-09 22:38 02b52000

View on Github →

chore: Rename Finset.piAntidiagonal to Finset.finsuppAntidiag (#13574) I need the version of this of type Finset (ι →₀ μ). I therefore rename the Finset (ι →₀ μ) from piAntidiagonal to finsuppAnttidiag since it's not about Pi but about Finsupp.

Estimated changes

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified Mathlib/Data/Finset/PiAntidiagonal.lean

added def Finset.finsuppAntidiag

added theorem Finset.finsuppAntidiag_empty

added theorem Finset.finsuppAntidiag_empty_of_ne_zero

added theorem Finset.finsuppAntidiag_empty_zero

added theorem Finset.finsuppAntidiag_insert

added theorem Finset.finsuppAntidiag_zero

added theorem Finset.mapRange_finsuppAntidiag_eq

added theorem Finset.mapRange_finsuppAntidiag_subset

deleted theorem Finset.mapRange_piAntidiagonal_eq

deleted theorem Finset.mapRange_piAntidiagonal_subset

added theorem Finset.mem_finsuppAntidiag'

added theorem Finset.mem_finsuppAntidiag

added theorem Finset.mem_finsuppAntidiag_insert

deleted theorem Finset.mem_piAntidiagonal'

deleted theorem Finset.mem_piAntidiagonal

deleted theorem Finset.mem_piAntidiagonal_insert

deleted def Finset.piAntidiagonal

deleted theorem Finset.piAntidiagonal_empty

deleted theorem Finset.piAntidiagonal_empty_of_ne_zero

deleted theorem Finset.piAntidiagonal_empty_of_zero

deleted theorem Finset.piAntidiagonal_insert

deleted theorem Finset.piAntidiagonal_zero

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified test/antidiagonal.lean