Commit 2024-11-29 03:48 27d7119d

View on Github →

chore(SetTheory/Ordinal/Basic): deprecate results on WellOrder (#18208) This PR is analogous to #18205.

Estimated changes

modified theorem Ordinal.type_def'
modified theorem Ordinal.type_def
modified theorem WellOrder.eta