Commit 2026-01-25 16:10 88a5ec11

View on Github →

chore: add deprecation for Cardinal.nat_lt_aleph0 (#34385) From #33990. Note that 4.27.0 was already released without this deprecation.

Estimated changes

added theorem Cardinal.nat_lt_aleph0