Commit 2026-09-01 10:17 1dabea3f

View on Github →

refactor(SetTheory/Ordinal): redefine Ordinal.ToType as Shrink (Iio o) (#42925) See conversation in #40725

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Basic.lean

deleted def Ordinal.ToType.mk

deleted def Ordinal.ToType

deleted def Ordinal.initialSegToType

deleted def Ordinal.principalSegToType

deleted def Ordinal.toTypeOrderBot

modified theorem Ordinal.type_toType