Commit 2024-06-15 08:18 f9ab9348

View on Github →

chore: Move antidiagonal material (#13727)

Rename Data.Finset.Antidiagonal to Algebra.Order.Antidiag.Prod
Rename Data.Finset.PiAntidiagonal to Algebra.Order.Antidiag.Finsupp
Move Finset.finAntidiag from the aforementioned to a new file Algebra.Order.Antidiag.Pi. This is in prevision of #13683.

Estimated changes

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified Mathlib.lean

Renamed Mathlib/Data/Finset/PiAntidiagonal.lean to Mathlib/Algebra/Order/Antidiag/Finsupp.lean

deleted def Finset.finAntidiagonal

deleted theorem Finset.mem_finAntidiagonal

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

added def Finset.finAntidiagonal

added theorem Finset.mem_finAntidiagonal

Renamed Mathlib/Data/Finset/Antidiagonal.lean to Mathlib/Algebra/Order/Antidiag/Prod.lean

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified test/antidiagonal.lean