Theorem Cardinal.isNormal_ord

Modification history

2025-08-22 21:50
Mathlib/SetTheory/Ordinal/Basic.lean
feat: `Cardinal.ord` is a normal function (#28752) …
Added Cardinal.isNormal_ordView on Github →