Commit 2024-12-03 05:50 72b0941b

View on Github →

chore: complete deprecation of PartENat.card (#19648)

depends on: #19622 (perhaps unnecessarily)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Subgroup/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

Modified Mathlib/Data/Finite/Card.lean

deleted theorem PartENat.card_eq_coe_natCard

Modified Mathlib/Data/Matroid/Basic.lean

Modified Mathlib/Data/Matroid/Closure.lean

Modified Mathlib/Data/Matroid/IndepAxioms.lean

Created Mathlib/Deprecated/Cardinal/Continuum.lean

added theorem Cardinal.aleph_toPartENat

added theorem Cardinal.continuum_toPartENat

Created Mathlib/Deprecated/Cardinal/Finite.lean

added theorem Cardinal.natCast_eq_toPartENat_iff

added theorem Cardinal.natCast_le_toPartENat_iff

added theorem Cardinal.natCast_lt_toPartENat_iff

added theorem Cardinal.toPartENat_eq_natCast_iff

added theorem Cardinal.toPartENat_le_natCast_iff

added theorem Cardinal.toPartENat_lt_natCast_iff

added def PartENat.card

added theorem PartENat.card_congr

added theorem PartENat.card_eq_coe_fintype_card

added theorem PartENat.card_eq_coe_natCard

added theorem PartENat.card_eq_top_of_infinite

added theorem PartENat.card_eq_zero_iff_empty

added theorem PartENat.card_image_of_injOn

added theorem PartENat.card_image_of_injective

added theorem PartENat.card_le_one_iff_subsingleton

added theorem PartENat.card_plift

added theorem PartENat.card_sum

added theorem PartENat.card_ulift

added theorem PartENat.one_lt_card_iff_nontrivial

Renamed Mathlib/SetTheory/Cardinal/PartENat.lean to Mathlib/Deprecated/Cardinal/PartENat.lean

Modified Mathlib/GroupTheory/Order/Min.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/NumberTheory/FLT/Three.lean

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

added theorem Cardinal.aleph_toENat

deleted theorem Cardinal.aleph_toPartENat

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Continuum.lean

added theorem Cardinal.continuum_toENat

deleted theorem Cardinal.continuum_toPartENat

Modified Mathlib/SetTheory/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_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