Theorem Ordinal.type_toPSet

Modification history

2025-12-08 05:19
Mathlib/SetTheory/ZFC/Ordinal.lean
refactor: `Ordinal.toType` → `Ordinal.ToType` (#32449) …
Modified Ordinal.type_toPSetView on Github →
2025-11-26 18:08
Mathlib/SetTheory/ZFC/Ordinal.lean
feat(SetTheory/ZFC/Ordinal): Lean ordinals to ZFC ordinals (#26544) …
Added Ordinal.type_toPSetView on Github →