Scope of mathlib

Stream: mathlib4

[Bolton Bailey]

My collaborator Pratyush has formalized the univariate sumcheck lemma as a part of our work on formalization of cryptographic proof systems. It's a lemma that ultimately only references elementary concepts:

lemma univariate_sumcheck {F : Type} [Field F] [Fintype F] {G : Subgroup Fˣ} {p : Polynomial F}
  {h_card_G : Fintype.card G ≥ 2} (σ : F) :
  ∑ x : G, Polynomial.eval (x.val.val) p = σ ↔
    ∃ h g,
      p = h * vanishingPoly G + ↑Polynomial.C (σ / ↑(Fintype.card G)) + Polynomial.X * g ∧
        Polynomial.natDegree g + 2 ≤ Fintype.card G ∧
          Polynomial.natDegree h ≤ Polynomial.natDegree p - Fintype.card G

In words, "The sum of a polynomial p over a multiplicative subgroup G of a field equals σ if and only if p is of the form h * V + σ/|G| + X * g, where V is the vanishing polynomial on the subgroup, g is a polynomial of degree at most |G|-2 and h is of degree a polynomial of degree at most |G| less than that of p".

You can see this theorem all around the SNARK literature (for example, as Fact 2 here), but I'm not sure where else I might expect to see it. I have been PRing prerequisites to mathlib over the past weeks. Does this theorem itself seem in scope for mathlib?

[Riccardo Brasca]

I don't see any problem in having it. And as you said you probable needed a few small missing lemmas that are very welcome to mathlib.