What kind of contributions should go to mathlib?

Stream: mathlib4

[Miguel Marco]

I decided to try the steps to contribute to mathlib, and decided to play around with a toy project: implement range'(that is, the natural numbers between aand a+b as Multisetand Finset (so we can have things like ∑ i in range' a b, f i ). Now i am doubting if this kind of things are supposed to be added to Mathlib or not.

Is there something like an "official criterion" about that?

[Yury G. Kudryashov]

We have docs#Finset.Ico and other intervals

[Yury G. Kudryashov]

I guess, the most "official" criterion is: not a duplicate and some maintainers think it's useful.

[Miguel Marco]

Thanks. Although I think that the genericFinset.Ico is missing some lemmas that hold specificially over the naturals (or maybe something slightly more general cases), and can be useful. Things like

Finset.Ico a (b + 1) = insert (a + b) (Finset.Ico a b)

Would it make sense to add this kind of thing?

[Ruben Van de Velde]

docs#Nat.Ico_succ_right_eq_insert_Ico ?

[Eric Wieser]

In general the bar for adding new theorems to mathlib is much lower than the bar for adding new definitions; but in both cases, it can take a while to work out whether the declaration you want already exists!

[Ruben Van de Velde]

Note that your range' is Ico a (a + b), not Ico a b

[Miguel Marco]

Ruben Van de Velde said:

docs#Nat.Ico_succ_right_eq_insert_Ico ?

Didn't see that. Thanks!

[Miguel Marco]

Eric Wieser said:

In general the bar for adding new theorems to mathlib is much lower than the bar for adding new definitions; but in both cases, it can take a while to work out whether the declaration you want already exists!

In case of theorems, i usually try to write the statement and then try to solve it with a tactic that searches the library (apply?, and/or aesop mostly). But apparently it is not as useful as I thought.

[Scott Morrison]

Make sure when testing with apply? that you have imported all of Mathlib in your test file. It only reports things visible with the current imports.

[Scott Morrison]

And asking in "Is there code for X?" is fine too, where Yaël, of whom apply? is just a lame imitiation, can usually tell you exactly where to find it.