Def Ordinal.toType.mk

Modification history

2025-12-08 05:19
Mathlib/SetTheory/Ordinal/Basic.lean
refactor: `Ordinal.toType` → `Ordinal.ToType` (#32449) …
Deleted Ordinal.toType.mkView on Github →
2025-12-05 15:16
Mathlib/SetTheory/Ordinal/Basic.lean
feat(SetTheory/Ordinal): Improve API for Ordinal.toType (#32408) …
Added Ordinal.toType.mkView on Github →