Commit 2025-08-22 21:50 55a28aa6

View on Github →

chore: reprove Ordinal.not_surjective_of_ordinal without Ordinal.lsub (#28751) Ordinal.lsub will soon be deprecated.

Estimated changes

modified theorem not_injective_of_ordinal
modified theorem not_surjective_of_ordinal