Commit 2025-07-25 18:35 c4b79e9f

View on Github →

refactor(SetTheory/Ordinal/Arithmetic): redefine Ordinal.IsNormal as Order.IsNormal (#26900) This is of course in anticipation to a subsequent PR that will deprecate Ordinal.IsNormal entirely.

Estimated changes

modified theorem Cardinal.isNormal_beth
modified theorem Cardinal.isNormal_preBeth
modified theorem Ordinal.IsNormal.strictMono
modified theorem Ordinal.isNormal_add_right
modified theorem Ordinal.isNormal_mul_right
modified theorem Ordinal.isNormal_opow