Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-22 20:06 9eb3858a

View on Github →

feat(combinatorics/pigeonhole): Pigeons in linear commutative rings (#13308) Duplicate almost all the pigeonhole principle API to work in linear_ordered_comm_rings.

Estimated changes

Modified src/algebra/module/basic.lean

added theorem finset.cast_card

Modified src/combinatorics/pigeonhole.lean

added theorem finset.exists_card_fiber_le_of_card_le_nsmul

added theorem finset.exists_card_fiber_lt_of_card_lt_nsmul

added theorem finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to

added theorem finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to

added theorem fintype.exists_card_fiber_le_of_card_le_nsmul

added theorem fintype.exists_card_fiber_lt_of_card_lt_nsmul

added theorem fintype.exists_le_card_fiber_of_nsmul_le_card

added theorem fintype.exists_lt_card_fiber_of_nsmul_lt_card