Commit 2023-02-11 15:47 b2668b1a

View on Github →

feat: Port Data.Finite.Card (#2183)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finite/Card.lean

added theorem Finite.card_eq

added theorem Finite.card_eq_zero_iff

added theorem Finite.card_eq_zero_of_embedding

added theorem Finite.card_eq_zero_of_injective

added theorem Finite.card_eq_zero_of_surjective

added theorem Finite.card_image_le

added theorem Finite.card_le_of_embedding'

added theorem Finite.card_le_of_embedding

added theorem Finite.card_le_of_injective'

added theorem Finite.card_le_of_injective

added theorem Finite.card_le_of_surjective'

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

added theorem Finite.card_pos_iff

added theorem Finite.card_range_le

added theorem Finite.card_subtype_le

added theorem Finite.card_subtype_lt

added theorem Finite.card_sum

added theorem Finite.cast_card_eq_mk

added def Finite.equivFin

added def Finite.equivFinOfCardEq

added theorem Finite.one_lt_card

added theorem Finite.one_lt_card_iff_nontrivial

added theorem Nat.card_eq

added theorem Set.card_union_le