Commit 2026-05-06 20:53 0a0340aa

View on Github →

feat: singular cardinals (#37098) We define a singular cardinal as an infinite cardinal which is larger than its cofinality. That's to say, every cardinal is exactly one of the following three: finite, regular, or singular.

Estimated changes

modified theorem Cardinal.aleph0_mul_aleph
modified theorem Cardinal.aleph_mul_aleph0
modified theorem Cardinal.IsInaccessible.pos
modified theorem Cardinal.IsRegular.cof_ord
modified theorem Cardinal.IsRegular.nat_lt
modified theorem Cardinal.IsRegular.ne_zero
modified theorem Cardinal.IsRegular.ord_pos
modified theorem Cardinal.IsRegular.pos
added structure Cardinal.IsSingular
modified theorem Cardinal.isInaccessible_def