Commit 2024-02-14 01:35 6f6928d4

View on Github →

feat(RingTheory/PowerSeries/Basic): coeff of products (#9309)

Use the class HasPiAntidiagonal defined in PR #7904 to compute the coefficients of products of power series (in several or one variable) : MvPowerSeries.coeff_prod and PowerSeries.coeff_prod
Update the file Archive/Partition.lean accordingly Co-author : Maria Ines de Frutos Fernandez Based on work of Bhavik Mehta in Archive/Partition.lean

Estimated changes

Modified Archive/Wiedijk100Theorems/Partition.lean

deleted theorem Theorems100.coeff_prod_range

deleted def Theorems100.cut

deleted theorem Theorems100.cut_empty_succ

deleted theorem Theorems100.cut_equiv_antidiag

deleted theorem Theorems100.cut_insert

deleted theorem Theorems100.cut_univ_fin_eq_antidiagonalTuple

deleted theorem Theorems100.cut_zero

deleted theorem Theorems100.mem_cut

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem AddEquiv.finsuppUnique_symm

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

added theorem MvPowerSeries.coeff_prod

added theorem PowerSeries.coeff_prod