Commit 2024-10-19 02:20 bd5ba6b8

View on Github →

chore(SetTheory/Ordinal/Basic): deprecate duplicate Nat.cast lemmas (#17857)

Estimated changes

modified theorem Ordinal.natCast_inj
modified theorem Ordinal.natCast_le