PR #18999: feat(order/irreducible): Sup-irreducible elements

Stream: triage

[Random Issue Bot]

Today I chose PR 18999 for discussion!

feat(order/irreducible): Sup-irreducible elements
Created by @Yaël Dillies (@YaelDillies) on 2023-05-12
Labels: awaiting-review, t-order

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

[Yaël Dillies]

Ready to be merged as far as I'm concerned