Contributing proof of Descartes' Rule of Signs

Stream: mathlib4

[Alex Meiburg]

Hey! I have a proof of the rule of signs: https://github.com/Timeroot/lean-descartes-signs/tree/main

Notably, this is one of the "100 problems to formalize" :) How do I go about, I dunno, getting any relevant stuff in mathlib, if that's wanted? I know several others of the 100 ended up in mathlib

[Utensil Song]

This thread has some related information about contributing it to Mathlib or adding it to the list of 100 problems for Lean formalizations.

[Yaël Dillies]

Feel free to request my review on PRs you open!

[Ruben Van de Velde]

It may be a bit much for a single PR, but it seems like auxiliary_defs.lean has a bunch of code that could be contributed separately. That's probably a good point to start

[Eric Rodriguez]

amazing! same with me as Yael - this was originally why I made SignType, actually. Why did you choose this proof?

[Alex Meiburg]

Yes, I separated out auxiliary_defs as the little facts that felt like it would be reasonable to put in mathlib even if the rest wasn't in a state to be merged. :)

[Alex Meiburg]

I guess I chose this one because it seemed like one I could reasonably do, as a way to force myself to learn Lean :P

[Ruben Van de Velde]

Seems to have worked :)

[Alex Meiburg]

It seems as though I should ask for write access to the central github (just not the master branch), instead of forking+PR?

[Ruben Van de Velde]

Yes, that's correct

[Alex Meiburg]

It looks as though statements like

theorem ext_get! [Inhabited α] (hl : length l₁ = length l₂)
  (h : ∀ n, get! l₁ n = get! l₂ n) : l₁ = l₂

theorem filter_replicate {f : α → Bool} :
  List.filter f (List.replicate n a) = if f a then List.replicate n a else []

would maybe belong in Std, is that correct? But maybe could go in Mathlib/Data/List/Basic.lean instead?

[Ruben Van de Velde]

Yeah, they could probably go into std, but we could also move them from mathlib to std later if needed