[Merged by Bors] - chore(Data/DFinsupp/Basic): remove impossible →ₚ notation

[negiizhao]

This is a binary operator that expands to a unary function; so this notation is (and has always been) impossible to use.

---

[grunweg]

To me, as a non-expert in this area, it's hard to judge whether this change is a good idea - as there's context missing.
Can you elaborate more why this notation makes no sense? (Or try to reconstruct when/why it was added in the first place?) Perhaps an expert in this area of mathlib will find this obvious, but I don't :-)

[negiizhao]

Just look at the type of DFinsupp : ∀ {ι : Type*} (β : ι → Type*) [(i : ι) → Zero (β i)], Type _. It's not a binary operation.

[eric-wieser]

bors merge

Thanks!

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style