Zulip Chat Archive
Stream: triage
Topic: PR #17879: feat(number_theory/modular_forms): gcomm_ring ...
Random Issue Bot (Jun 30 2023 at 14:07):
Today I chose PR 17879 for discussion!
feat(number_theory/modular_forms): gcomm_ring instance
Created by @Chris Birkbeck (@CBirkbeck) on 2022-12-09
Labels: WIP
Is this PR still relevant? Any recent updates? Anyone making progress?
Chris Birkbeck (Jun 30 2023 at 14:08):
Yes this is still relevant. I'm just waiting to port this to mathlib4 once I've finished with some Eisenstein series things.
Random Issue Bot (Aug 10 2023 at 14:08):
Today I chose PR 17879 for discussion!
feat(number_theory/modular_forms): gcomm_ring instance
Created by @Chris Birkbeck (@CBirkbeck) on 2022-12-09
Labels: WIP, too-late
Is this PR still relevant? Any recent updates? Anyone making progress?
Chris Birkbeck (Aug 10 2023 at 14:08):
I'm porting this to Lean4, so maybe it can be closed? (as this was a lean3 PR?)
Eric Wieser (Aug 10 2023 at 14:35):
Please ping me for review once it gets there!
Last updated: Dec 20 2023 at 11:08 UTC