Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-19 02:36 aedbc12e

View on Github →

feat(data/fintype): card lemmas (#168)

Estimated changes

Modified algebra/big_operators.lean

added theorem finset.card_pi

added theorem finset.prod_const

added theorem finset.sum_const

Modified data/fintype.lean

added theorem fintype.card_eq_one_iff

added theorem fintype.card_eq_zero_iff

added theorem fintype.card_fun

added theorem fintype.card_le_of_injective

added theorem fintype.card_le_one_iff

added theorem fintype.card_pi

added theorem fintype.card_pos_iff