Commit 2026-03-25 05:05 9ab11f2e

View on Github →

chore: remove declarations deprecated between 2021-03-24 and 2025-09-24 (#37118) I am happy to remove some deprecated declarations for you! Please check if there are any remaining stray comments or other issues before merging.

Estimated changes

deleted theorem Finset.mem_sum
deleted theorem div_add_div_same
deleted theorem Equiv.Perm.apply_inv_self
deleted theorem Equiv.Perm.inv_apply_self
deleted theorem divp_assoc'
deleted theorem Matrix.PosSemidef.sq_sqrt
deleted theorem Matrix.PosSemidef.sqrt_sq
deleted theorem Finset.ofColex_injective
deleted theorem Finset.ofColex_ne_ofColex
deleted theorem Finset.toColex_injective
deleted theorem Finset.toColex_ne_toColex
deleted theorem Finset.range_succ
deleted theorem Set.encard_univ_coe
deleted theorem Subtype.ext_iff_val
deleted theorem Subtype.ext_val
deleted theorem Equiv.Perm.image_inv
deleted theorem Equiv.Perm.preimage_inv
deleted theorem Matrix.dotProduct_empty
deleted theorem iSupIndep_empty
deleted theorem iSupIndep_pempty
deleted theorem IsAdjoinRoot.subsingleton
deleted def AddValuation.asFun
deleted theorem Ordinal.mul_right_inj
deleted theorem AffineMap.continuous_iff