PR !4#16925: feat(SetTheory/Cardinal/Cofinality): aleph i...

Stream: triage

[Random Issue Bot]

Today I chose PR 16925 for discussion!

feat(SetTheory/Cardinal/Cofinality): aleph index of singular cardinal has infinite cofinality
Created by @None (@YnirPaz) on 2024-09-18
Labels: WIP, merge-conflict, t-set-theory

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

[Violeta Hernández]

This depends on us defining IsSingular first.

[Violeta Hernández]

And defining IsSingular depends on us moving all the stuff on regular cardinals to its separate file. I'll try and get that done.