mathlib

9eb3858a - feat(combinatorics/pigeonhole): Pigeons in linear commutative rings (#13308)

feat(combinatorics/pigeonhole): Pigeons in linear commutative rings (#13308) Duplicate almost all the pigeonhole principle API to work in `linear_ordered_comm_ring`s. Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>