Def Ordinal.ToType.mk

Modification history

2025-12-08 05:19
Mathlib/SetTheory/Ordinal/Basic.lean
refactor: `Ordinal.toType` → `Ordinal.ToType` (#32449) …
Added Ordinal.ToType.mkView on Github →