Commit 2026-08-31 13:50 738f2ab1

View on Github →

chore: delete deprecated declarations from February 2026 (#43178) #42655 is still stuck; this is a manual removal while improvements are being worked on (cf. #mathlib4 > Automated deprecation removal not working @ 💬). Mathlib.Data.Finsupp.PointwiseSMul is deleted because all declarations in it are deprecated and over 6 months old.

Estimated changes

deleted theorem SemimoduleCat.forget_map
deleted theorem Fin.coe_covBy_iff
deleted inductive IsSolvableByRad
deleted theorem Zsqrtd.le_antisymm
deleted def AntiSymmetric
deleted def Irreflexive
deleted def Total
deleted def Transitive
deleted theorem transitive_of_trans
deleted theorem Set.Icc_union_Ici'
deleted theorem Set.Ico_union_Ici'
deleted theorem Set.Iic_union_Icc'
deleted theorem Set.Iic_union_Ioc'
deleted theorem Set.Iio_union_Ico'
deleted theorem Set.Iio_union_Ioo'
deleted theorem Set.Ioc_union_Ioi'
deleted theorem Set.Ioo_union_Ioi'
deleted theorem IsChain.image_embedding
deleted theorem IsChain.image_iso
deleted theorem IsChain.image_relIso
deleted theorem Ordinal.cof_ne_zero
deleted theorem Ordinal.div_lt
deleted theorem Ordinal.le_div
deleted theorem Ordinal.add_one_eq_succ
deleted theorem Ordinal.add_succ
deleted theorem Ordinal.card_succ
deleted theorem Ordinal.induction
deleted theorem Ordinal.succ_ne_zero
deleted theorem Ordinal.succ_one
deleted theorem Ordinal.succ_zero
deleted theorem Ordinal.veblenWith_succ
deleted theorem Ordinal.veblen_succ
deleted theorem Ordinal.toZFSet_succ