Commit 2023-02-11 15:25 68d985ac

View on Github →

feat: Port SetTheory.Cardinal.Finite (#2182)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Nat.card_congr

added theorem Nat.card_eq_fintype_card

added theorem Nat.card_eq_of_bijective

added theorem Nat.card_eq_of_equiv_fin

added theorem Nat.card_eq_one_iff_unique

added theorem Nat.card_eq_two_iff'

added theorem Nat.card_eq_two_iff

added theorem Nat.card_eq_zero_of_infinite

added theorem Nat.card_fun

added theorem Nat.card_of_isEmpty

added theorem Nat.card_of_subsingleton

added theorem Nat.card_pLift

added theorem Nat.card_pi

added theorem Nat.card_prod

added theorem Nat.card_uLift

added theorem Nat.card_unique

added theorem Nat.card_zMod

added def Nat.equivFinOfCardPos

added theorem Nat.finite_of_card_ne_zero

added def PartENat.card

added theorem PartENat.card_eq_coe_fintype_card

added theorem PartENat.card_eq_top_of_infinite