Commit 2025-07-12 06:00 628f8247

View on Github →

chore: remove >6 month old material in Deprecated (#25790)

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Deprecated/Cardinal/Continuum.lean

deleted theorem Cardinal.aleph_toPartENat

deleted theorem Cardinal.continuum_toPartENat

Deleted Mathlib/Deprecated/Cardinal/Finite.lean

deleted theorem Cardinal.natCast_eq_toPartENat_iff

deleted theorem Cardinal.natCast_le_toPartENat_iff

deleted theorem Cardinal.natCast_lt_toPartENat_iff

deleted theorem Cardinal.toPartENat_eq_natCast_iff

deleted theorem Cardinal.toPartENat_le_natCast_iff

deleted theorem Cardinal.toPartENat_lt_natCast_iff

deleted def PartENat.card

deleted theorem PartENat.card_congr

deleted theorem PartENat.card_eq_coe_fintype_card

deleted theorem PartENat.card_eq_coe_natCard

deleted theorem PartENat.card_eq_top_of_infinite

deleted theorem PartENat.card_eq_zero_iff_empty

deleted theorem PartENat.card_image_of_injOn

deleted theorem PartENat.card_image_of_injective

deleted theorem PartENat.card_le_one_iff_subsingleton

deleted theorem PartENat.card_plift

deleted theorem PartENat.card_sum

deleted theorem PartENat.card_ulift

deleted theorem PartENat.one_lt_card_iff_nontrivial

Deleted Mathlib/Deprecated/Cardinal/PartENat.lean

deleted theorem Cardinal.aleph0_toPartENat

deleted theorem Cardinal.mk_toPartENat_eq_coe_card

deleted theorem Cardinal.mk_toPartENat_of_infinite

deleted theorem Cardinal.partENatOfENat_toENat

deleted theorem Cardinal.toPartENat_apply_of_aleph0_le

deleted theorem Cardinal.toPartENat_apply_of_lt_aleph0

deleted theorem Cardinal.toPartENat_congr

deleted theorem Cardinal.toPartENat_eq_top

deleted theorem Cardinal.toPartENat_inj_of_le_aleph0

deleted theorem Cardinal.toPartENat_le_iff_of_le_aleph0

deleted theorem Cardinal.toPartENat_le_iff_of_lt_aleph0

deleted theorem Cardinal.toPartENat_lift

deleted theorem Cardinal.toPartENat_mono

deleted theorem Cardinal.toPartENat_natCast

deleted theorem Cardinal.toPartENat_strictMonoOn

deleted theorem Cardinal.toPartENat_surjective

Modified Mathlib/Deprecated/Order.lean