PR !4#12744: feat(RingTheory/Smooth): Noetherian ring of ...

Stream: triage

[Random Issue Bot]

Today I chose PR #12744 for discussion!

feat(RingTheory/Smooth): Noetherian ring of definition
Created by @Christian Merten (@chrisflav) on 2024-05-07
Labels: merge-conflict, t-ring-theory

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

[Johan Commelin]

This is a draft PR. Can we teach the triage bot to ignore those?

[Bhavik Mehta]

On that note, can we make it ignore things which are too new, or have had recent discussion?

[Bryan Gin-ge Chen]

I updated the bot to filter out drafts earlier today (azure-scripts#49). It should already be filtering out issues / PRs which have an updated_at field within the last 7 days (see this line and the analogous one in the PR filtering section). Should we change that to 14 days?

[Bhavik Mehta]

Ah okay, 7 days is probably enough I think. Thanks!