Mathlib v3 is deprecated. Go to Mathlib v4

Theorem configuration.has_lines.exists_unique_line

Modification history

2021-12-17 12:31
src/combinatorics/configuration.lean
feat(combinatorics/configuration): New file (#10773) …
Added configuration.has_lines.exists_unique_lineView on Github →