Sidon sets

[b-mehta]

The formulation of Sidon sets currently in the repo is not right for mathlib:

• It works with sequences rather than sets. Historically in combinatorial number theory (as it was called then), infinite sets of naturals were usually expressed as strictly monotone sequences, but the modern formulation is to use infinite sets directly instead, and so the mathlib version should do the latter too.
• As a result, it requires a Sidon set to be infinite, and so is not a useful formulation for cases like ZMod n or other finite abelian groups, which are cases studied in the literature.

These are not correctness problems however: the problem statements using Sidon sets are taking in a valid assumption.

[b-mehta]

If the GDM team agrees this should be changed here then I'm happy to work on it. Alternatively, since the current Erdos problems set works fine with this definition, I'm happy just to put the improved definition in mathlib, then this repo can be adjusted after the fact. Your call!

[mo271]

I agree this should be changed, handling the increased sequences is a bit awkward, infinite sets sounds better.

Both options sound good: fixing the improved definition in ForMathlib of this repo first or in parallel of upstreaming to mathlib is perhaps a good idea, since we don't get the benefits upstream changes to mathlib immediately, because we follow stable versions.
Thanks for working on it, @b-mehta!

[eric-wieser]

since we don't get the benefits upstream changes to mathlib immediately, because we follow stable versions.

Interpreting this another way; you have three days to upstream this before the next stable mathlib release is cut!