Def Ordinal.toTypeOrderBotOfPos

Modification history

2025-09-08 07:33

Mathlib/SetTheory/Ordinal/Basic.lean

chore: remove >6 month deprecations (#29276) …

Deleted Ordinal.toTypeOrderBotOfPos View on Github →

2024-08-27 18:38

Mathlib/SetTheory/Ordinal/Basic.lean

chore(SetTheory/Ordinal/*): `o.out.α` → `o.toType` (#16161) …

Added Ordinal.toTypeOrderBotOfPos View on Github →