Zulip Chat Archive

Stream: triage

Topic: PR #4956: feat(archive/imo): formalise 1979 Q1

Random Issue Bot (Dec 10 2021 at 14:20):

Today I chose PR 4956 for discussion!

feat(archive/imo): formalise 1979 Q1
Created by @Kevin Buzzard (@kbuzzard) on 2020-11-09
Labels: awaiting-author, imo

Is this PR still relevant? Any recent updates? Anyone making progress?

Kevin Buzzard (Dec 10 2021 at 19:13):

I can imagine getting back to this one day. I only recently noticed that it was still dangling when I made another PR and then clicked on "my open PRs" and found to my surprise that I had two!

Random Issue Bot (Mar 13 2022 at 14:12):

Today I chose PR 4956 for discussion!

feat(archive/imo): formalise 1979 Q1
Created by @Kevin Buzzard (@kbuzzard) on 2020-11-09
Labels: awaiting-author, imo

Is this PR still relevant? Any recent updates? Anyone making progress?

Kevin Buzzard (Mar 13 2022 at 15:16):

@Yaël Dillies why did you reopen this?

Yaël Dillies (Mar 13 2022 at 15:18):

Because I added all the finset.Ixx stuff. The one thing left to be done is to switch to the p-adic norm, although IMO it's not necessary.

Last updated: Dec 20 2023 at 11:08 UTC