mathlib3

e839c9ae - feat(combinatorics/configuration): Cardinality results for projective plane. (#11406)

feat(combinatorics/configuration): Cardinality results for projective plane. (#11406) This PR proves several cardinality results for projective planes (e.g., number of points = number of lines, number of points on given line = number of lines on given point). It looks like the `exists_config` (whose sole purpose is to rule out [the 7th example here](https://en.wikipedia.org/wiki/Projective_plane#Degenerate_planes)) can be weakened slightly.