Zulip Chat Archive

Stream: triage

Topic: PR #9606: feat(ring_theory/euclidean_domain): generalize ...


Random Issue Bot (Nov 07 2021 at 14:18):

Today I chose PR 9606 for discussion!

feat(ring_theory/euclidean_domain): generalize lemmas to PIDs
Created by @Ruben Van de Velde (@Ruben-VandeVelde) on 2021-10-07
Labels: awaiting-author

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

Ruben Van de Velde (Nov 07 2021 at 14:19):

Not making progress, no :(

Anne Baanen (Nov 08 2021 at 11:44):

I fixed another timeout, hopefully.


Last updated: Dec 20 2023 at 11:08 UTC