Commit 2024-10-14 09:30 3f919e0d

View on Github →

chore(SetTheory/Ordinal/Arithmetic): sub_isNormal → isNormal_sub, etc. (#17673) We fix various misnamed lemmas involving IsNormal and IsLimit.

Estimated changes

added theorem Cardinal.isNormal_beth
deleted theorem Ordinal.add_isLimit
deleted theorem Ordinal.add_isNormal
added theorem Ordinal.isLimit_add
added theorem Ordinal.isLimit_mul
added theorem Ordinal.isLimit_sub
deleted theorem Ordinal.mul_isLimit
deleted theorem Ordinal.mul_isLimit_left
deleted theorem Ordinal.mul_isNormal
deleted theorem Ordinal.sub_isLimit
added theorem Ordinal.isLimit_opow
added theorem Ordinal.isNormal_opow
deleted theorem Ordinal.opow_isLimit
deleted theorem Ordinal.opow_isLimit_left
deleted theorem Ordinal.opow_isNormal
deleted theorem Ordinal.deriv_isNormal
added theorem Ordinal.isNormal_deriv