mathlib3

c0e613a2 - feat(combinatorics/configuration): `nondegenerate.exists_injective_of_card_le` (#11019)

feat(combinatorics/configuration): `nondegenerate.exists_injective_of_card_le` (#11019) If a nondegenerate configuration has at least as many points as lines, then there exists an injective function `f` from lines to points, such that `f l` does not lie on `l`. This is the key lemma for #10772. The proof is an application of Hall's marriage theorem.