Commit 2026-04-17 13:01 05036b80

View on Github →

chore: deprecate various theorems about Ordinal.ToType (#37972) We should generally be writing theorems about "well-orders of order type o", rather than theorems about o.ToType (which is just one such well-order, defined via choice).

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

Modified Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

Modified Mathlib/FieldTheory/CardinalEmb.lean

Modified Mathlib/SetTheory/Cardinal/Order.lean

modified theorem Cardinal.succ_pos

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Cardinal.noMaxOrder

Modified Mathlib/SetTheory/Ordinal/Basic.lean