Commit 2026-10-16 07:34 ce44de8b

View on Github →

chore: remove declarations deprecated between 2026-04-01 and 2026-04-15 (#44903) This robot [dubious – discuss] is happy to remove some deprecated declarations for you! Please check if there are any remaining stray comments or other issues before merging. This PR is #44886 plus some manual fixes.

Estimated changes

deleted theorem Condensed.comp_hom
deleted theorem Condensed.id_hom
deleted theorem LightCondensed.comp_hom
deleted theorem LightCondensed.id_hom
deleted theorem String.toList_nonempty
deleted def Module.dualPairing
deleted theorem Module.dualPairing_apply
deleted def LinearOrder.swap
deleted theorem PMF.bernoulli_expectation
deleted theorem Cardinal.bddAbove_range
deleted theorem Ordinal.add_one_ne_zero
deleted theorem Ordinal.enum_zero_eq_bot
deleted theorem Ordinal.succ_pos
deleted theorem Ordinal.IsNormal.bsup
deleted theorem Ordinal.bddAbove_range
deleted def Ordinal.brange
deleted theorem Ordinal.brange_const
deleted theorem Ordinal.bsup'_eq_iSup
deleted def Ordinal.bsup
deleted theorem Ordinal.bsup_congr
deleted theorem Ordinal.bsup_const
deleted theorem Ordinal.bsup_eq_bsup
deleted theorem Ordinal.bsup_eq_iSup
deleted theorem Ordinal.bsup_eq_zero_iff
deleted theorem Ordinal.bsup_le
deleted theorem Ordinal.bsup_le_iff
deleted theorem Ordinal.bsup_one
deleted theorem Ordinal.bsup_succ_of_mono
deleted theorem Ordinal.bsup_zero
deleted theorem Ordinal.iSup'_eq_bsup
deleted theorem Ordinal.iSup_Iio_eq_bsup
deleted theorem Ordinal.iSup_eq_bsup
deleted theorem Ordinal.iSup_eq_iSup
deleted theorem Ordinal.le_bsup
deleted theorem Ordinal.lt_bsup
deleted theorem Ordinal.lt_bsup_of_limit
deleted theorem Ordinal.mem_brange
deleted theorem Ordinal.mem_brange_self
deleted theorem Ordinal.sSup_eq_bsup
deleted theorem Ordinal.isClosed_iff_bsup