Commit 2025-02-20 09:21 d3e5cce2

View on Github →

chore(Data/Fintype): split Fintype/Card.lean (#21840) This PR splits Data.Fintype.Card based on dependencies:

  • Data.Fintype.Card contains the definition of Fintype.card and basic results
  • Data.Fintype.EquivFin contains the equivalences between fintypes, finiteness and Fin
  • Data.Fintype.Pigeonhole contains a few pigeonhole principles
  • Data.Fintype.Group gets a few extra results on Additive/Multiplicative

Estimated changes

added theorem Fintype.card_additive
deleted theorem Finite.of_injective
deleted theorem Finite.of_surjective
deleted theorem Finset.card_eq_of_equiv
deleted theorem Finset.exists_maximal
deleted theorem Finset.exists_minimal
deleted theorem Finset.univ_map_embedding
deleted theorem Fintype.card_additive
deleted theorem Fintype.card_eq
deleted theorem Fintype.card_eq_one_iff
deleted theorem Fintype.card_le_one_iff
deleted theorem Fintype.card_quotient_lt
deleted theorem Fintype.one_lt_card
deleted theorem Fintype.one_lt_card_iff
deleted theorem Infinite.of_injective
deleted theorem Infinite.of_not_fintype
deleted theorem Infinite.of_surjective
deleted theorem Infinite.sigma_of_right
deleted theorem isEmpty_fintype
added theorem Finite.of_injective
added theorem Finite.of_surjective
added theorem Finset.exists_maximal
added theorem Finset.exists_minimal
added theorem Fintype.card_eq
added theorem Fintype.one_lt_card
added theorem Infinite.of_injective
added theorem Infinite.of_surjective
added theorem isEmpty_fintype