Introduction and PR access request

Stream: new members

[Keke Zhang]

Hi everyone! I’m a final year PhD student in mathematical physics at Perimeter Institute. I am interested in formalizing some foundational representation theory in Lean, with a long-term eye toward geometric Langlands. My short term goal is to formalize contents of the Quantum Hikita Conjecture.

As a starting point, I've written a coordinate-free construction of the Weyl algebra (affine $\mathcal{D}$-modules) over a commutative ring using TensorAlgebra and RingQuot.

I would love to start contributing this to mathlib. Could I please get push access to non-master branches? My GitHub username is Kekedile.

[Snir Broshi]

Hello! Contributors no longer get push access, but rather create PRs from forks: https://leanprover-community.github.io/contribute/git.html#open-a-pull-request

[Yan Yablonovskiy 🇺🇦]

Whilst not directly related what you said , you may be interested in GibbsMeasure , and more broadly related is PhysLean .