Commit 2025-12-08 05:19 4ed94053

View on Github →

refactor: Ordinal.toType → Ordinal.ToType (#32449) See Zulip.

Estimated changes

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

Modified Mathlib/CategoryTheory/Presentable/CardinalFilteredPresentation.lean

Modified Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean

Modified Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

modified theorem CategoryTheory.OrthogonalReflection.iteration_map_succ

modified theorem CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity

modified theorem CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity

Modified Mathlib/CategoryTheory/SmallObject/Basic.lean

Modified Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

modified theorem CategoryTheory.SmallObject.hasIterationOfShape

modified theorem CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left

modified theorem CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ιIteration_app_right

modified theorem CategoryTheory.SmallObject.prop_iterationFunctor_map_succ

modified theorem CategoryTheory.SmallObject.ιFunctorObj_eq

modified theorem CategoryTheory.SmallObject.πFunctorObj_eq

Modified Mathlib/CategoryTheory/SmallRepresentatives.lean

Modified Mathlib/FieldTheory/CardinalEmb.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Ordinal.cof_eq_cof_toType

Modified Mathlib/SetTheory/Cardinal/Ordinal.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/SetTheory/Game/Nim.lean

modified theorem SetTheory.PGame.leftMoves_nim

modified theorem SetTheory.PGame.rightMoves_nim

Modified Mathlib/SetTheory/Game/Ordinal.lean

modified theorem Ordinal.toPGame_leftMoves

Modified Mathlib/SetTheory/Nimber/Field.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

modified theorem Cardinal.noMaxOrder

modified theorem Ordinal.toType_noMax_of_succ_lt

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified theorem Cardinal.card_typein_toType_lt

modified theorem Cardinal.mk_Iio_ord_toType

modified theorem Cardinal.mk_ord_toType

modified theorem Cardinal.mk_toType

added def Ordinal.ToType.mk

added def Ordinal.ToType

modified theorem Ordinal.enum_zero_le'

modified def Ordinal.initialSegToType

modified theorem Ordinal.le_enum_succ

modified theorem Ordinal.one_toType_eq

modified def Ordinal.principalSegToType

deleted def Ordinal.toType.mk

deleted def Ordinal.toType

modified def Ordinal.toTypeOrderBot

modified theorem Ordinal.toType_empty_iff_eq_zero

modified theorem Ordinal.toType_nonempty_iff_ne_zero

modified theorem Ordinal.type_toType

modified theorem Ordinal.typein_le_typein'

modified theorem Ordinal.typein_lt_self

modified theorem Ordinal.typein_one_toType

Modified Mathlib/SetTheory/Ordinal/Family.lean

modified def Ordinal.familyOfBFamily

modified theorem Ordinal.lsub_typein

Modified Mathlib/SetTheory/ZFC/Ordinal.lean

modified theorem Ordinal.type_toPSet