PR !4#12768: feat: two equiv involving `Associates` and `...

Stream: triage

[Random Issue Bot]

Today I chose PR 12768 for discussion!

feat: two equiv involving Associates and nonZeroDivisors
Created by @Xavier Roblot (@xroblot) on 2024-05-08
Labels: awaiting-review, t-algebra

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

[Kevin Buzzard]

I hope it's still relevant -- it's only 10 days old! Are we really supposed to be triaging PRs like this?

[Yaël Dillies]

Makes me click and review, so :shrug: