mathlib

d28b3bd5 - feat(combinatorics/configuration): Points and lines inequality (#10772)

feat(combinatorics/configuration): Points and lines inequality (#10772) If a nondegenerate configuration has a unique line through any two points, then there are at least as many lines as points.