Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-01 03:11 f060e09c

View on Github →

chore(*): golf some proofs (#5983) API changes:

  • new lemmas finset.card_filter_le, finset.compl_filter, finset.card_lt_univ_of_not_mem, fintype.card_le_of_embedding, fintype.card_lt_of_injective_not_surjective;
  • rename finset.card_le_of_inj_on → finset.le_card_of_inj_on_range;
  • rename card_lt_of_injective_of_not_mem to fintype.card_lt_of_injective_of_not_mem;
  • generalize card_units_lt to a monoid_with_zero.

Estimated changes

added theorem finset.card_filter_le
deleted theorem finset.card_le_of_inj_on
added theorem finset.compl_filter
modified theorem set.range_inclusion
modified theorem card_units_lt