Commit 2025-03-11 00:25 00d98b7f

chore(SetTheory/Cardinal/Cofinality): split file (#21972) The cofinality file is currently a hodgepodge of different results and definitions. We split it as follows:

• Regular and inaccessible cardinals are moved to SetTheory.Cardinal.Regular. This file will also be used to define singular cardinals in the near future.
• The infinite pigeonhole principle gets its own file. It would've been nice to move ordinal fundamental sequences as well, but they're currently (unnecessarily) used to prove some results on cofinality. A future refactor #19698 will take care of this.