Commit 2025-07-01 00:55 1a5c8fe5

View on Github →

chore: bump toolchain to v4.22.0-rc2 (#26564) This merged the reviewed changes from bump/v4.22.0, and updates Mathlib to use the v4.22.0-rc2 toolchain.

Estimated changes

modified theorem CharP.cast_eq_mod
modified theorem Finset.smul_finset_empty
deleted def AdjoinRoot.evalEval
modified theorem CategoryTheory.forget_obj
modified theorem DFinsupp.coe_piecewise
modified theorem ENNReal.top_sub_coe
modified theorem Int.natCast_mod
deleted theorem List.idxOf_le_length
deleted theorem List.idxOf_lt_length_iff
deleted theorem List.insertIdx_eraseIdx
added theorem List.nodup_append'
deleted theorem List.nodup_append
modified theorem Stream'.Seq.val_eq_get
modified theorem Stream'.append_eq_cons
modified theorem Sum.Ioo_inl_inr
modified theorem Sum.Ioo_inr_inl
deleted def ContinuousMap.toLp
deleted def PMF.binomial
modified def importId