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

Stream: triage

[Random Issue Bot]

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]

Not making progress, no :(

[Anne Baanen]

I fixed another timeout, hopefully.