Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-22 18:31 d8fc588d

View on Github →

refactor(data/finite/card): split from basic (#14885)

Estimated changes

Modified src/data/finite/basic.lean

deleted theorem finite.card_eq

deleted theorem finite.card_eq_zero_iff

deleted theorem finite.card_le_of_embedding

deleted theorem finite.card_le_of_injective

deleted theorem finite.card_le_of_surjective

deleted theorem finite.card_le_one_iff_subsingleton

deleted theorem finite.card_option

deleted theorem finite.card_pos_iff

deleted theorem finite.card_subtype_le

deleted theorem finite.card_subtype_lt

deleted theorem finite.card_sum

deleted def finite.equiv_fin

deleted def finite.equiv_fin_of_card_eq

deleted theorem finite.one_lt_card

deleted theorem finite.one_lt_card_iff_nontrivial

deleted theorem nat.card_eq

Created src/data/finite/card.lean

added theorem finite.card_eq

added theorem finite.card_eq_zero_iff

added theorem finite.card_le_of_embedding

added theorem finite.card_le_of_injective

added theorem finite.card_le_of_surjective

added theorem finite.card_le_one_iff_subsingleton

added theorem finite.card_option

added theorem finite.card_pos_iff

added theorem finite.card_subtype_le

added theorem finite.card_subtype_lt

added theorem finite.card_sum

added def finite.equiv_fin

added def finite.equiv_fin_of_card_eq

added theorem finite.one_lt_card

added theorem finite.one_lt_card_iff_nontrivial

added theorem nat.card_eq