Commit 2025-12-05 15:16 69f968a9

View on Github →

feat(SetTheory/Ordinal): Improve API for Ordinal.toType (#32408) Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/API.20for.20Ordinal.2EtoType/with/561739587

  • Adds coercion from Ordinal.toType to Ordinal & Set.Iio o
  • Renames Ordinal.enumIsoToType to Ordinal.toType.mk with an implicit parameter, so (.mk ⟨α, h⟩) can be used to build a toType. This prepares for deprecation of the name Ordinal.enumIsoToType (to be discussed).

Estimated changes