Contributing Groebner Basis to Mathlib

Stream: new members

[tsuki（Hao Shen)]

Hi!
I've recently been working on Groebner bases on https://github.com/WuProver/groebner_proj with @Hagb (Junyu Guo) . I'm planning to gradually contribute some lemmas and our main works to the Mathlib library. My GitHub username is tsuki8. Could anyone grant me write access to non-master branches of Mathlib4, please?

[Jeremy Tan]

@Leonardo de Moura is already working on Gröbner bases in Lean proper

[Eric Wieser]

I think the plan in Lean core is to build tactics that use Grobner bases, not to formalize their semantics