Commit 2025-02-13 14:43 2278a542
View on Github →feat(SetTheory): regular cardinals have a least element (#21780)
Ordinal.toTypeOrderBotOfPos is deprecated in favour of a new definition Ordinal.toTypeOrderBotOfPos which takes an assumption o ≠ 0. A similar definition is introduced for cardinals, and a lemma Cardinal.IsRegular.ne_zero is added. As a result, if c is a regular cardinal, then c.ord.toType has a least element.