Commit 2025-05-08 18:26 4c30fbb1

feat(Data/Finsupp/Basic): add Finsupp.(un)curry_single and @[simps] to Finsupp.finsuppProd(L)Equiv (#23021) This was raised by @Whysoserioushah regarding #21732. We add Finsupp.uncurry_apply, which simplifies Finsupp.uncurry applied to a term of a product type xy : α × β, to prevent Basis.smulTower_repr breaking. However, we don't tag this with @[simp]; there is already a @[simp] tag on the less eager Finsupp.uncurry_apply_pair, which applies to a pair of terms x : α, y : β.