PR !4#18206: chore(SetTheory/Ordinal/Basic): golf/clean u...

Stream: triage

[Random Issue Bot]

Today I chose PR #18206 for discussion!

chore(SetTheory/Ordinal/Basic): golf/clean up Cardinal.ord theorems
Created by @Violeta Hernández (@vihdzp) on 2024-10-24
Labels: awaiting-author, merge-conflict, t-set-theory

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

[Violeta Hernández]

Still relevant, I'll clean this up later today.