Commit 2025-12-26 17:05 0bf098ca

View on Github →

refactor: deprecate Ordinal.IsNormal for Order.IsNormal (#33294)

Estimated changes

deleted theorem Ordinal.IsNormal.cof_eq
deleted theorem Ordinal.IsNormal.cof_le
modified theorem Ordinal.IsNormal.id_le
modified theorem Ordinal.IsNormal.inj
modified theorem Ordinal.IsNormal.le_apply
modified theorem Ordinal.IsNormal.le_iff
modified theorem Ordinal.IsNormal.le_iff_eq
modified theorem Ordinal.IsNormal.le_set'
modified theorem Ordinal.IsNormal.le_set
modified theorem Ordinal.IsNormal.limit_le
modified theorem Ordinal.IsNormal.limit_lt
modified theorem Ordinal.IsNormal.lt_iff
modified theorem Ordinal.IsNormal.monotone
modified theorem Ordinal.IsNormal.refl
modified theorem Ordinal.IsNormal.strictMono
modified theorem Ordinal.IsNormal.trans
deleted def Ordinal.IsNormal
deleted theorem Ordinal.iSup_pow
modified theorem Ordinal.isNormal_opow
modified theorem Ordinal.IsNormal.map_iSup
deleted theorem Ordinal.iSup_add_nat
deleted theorem Ordinal.iSup_mul_nat
deleted theorem Ordinal.IsNormal.deriv_fp
deleted theorem Ordinal.IsNormal.nfp_fp
added theorem Ordinal.apply_le_nfp
added theorem Ordinal.apply_lt_nfp
added theorem Ordinal.deriv_fp
added theorem Ordinal.fp_iff_deriv
added theorem Ordinal.le_iff_deriv
added theorem Ordinal.nfp_fp
added theorem Ordinal.nfp_le_apply