BigOp binders

Stream: mathlib4

[Yuval Filmus]

BigOps support various binders, such as summing over all elements in some set, all elements at most something, and so on.
Here are two that I find missing:

1. Summing over all elements not in some set. This can be simulated using set complement notation.
2. Summing over all elements different from some element. This can be simulated using univ.erase.

Both of these features are easy to add by modifying processBigOpBinder in Algebra.BigOperators.Group.Finset.Defs.
Does this sound like a good idea?

[Yaël Dillies]

Yes absolutely! Please coordinate with #22048 :smile:

[Yuval Filmus]

For starters, can I please have write access to non-master branches, per the guide?

[Kim Morrison]

@Yuval Filmus, can you please add your github username to your zulip profile?

[Yuval Filmus]

@Kim Morrison Done

[Kevin Buzzard]

@Yuval Filmus invitation sent!